Prod.mk_lt_mk

Exact source identity

Canonical occurrence

object-ddf75e09858e62cc4a6927116dcb557c5c6f4b63f96f8c57caa300979368c37a

Kind

theorem

Module

Mathlib.Order.Basic

Path

Mathlib/Order/Basic.lean

Repository

https://github.com/leanprover-community/mathlib4

Commit

d13f23b723b8a846827a245b89c10fc7d3f11612

Tree

efa132418a56d0e38c56cc412a06df22178dac5c

Statement digest

7f0f95415ce55c54f20645371ed01ceb8472b5cf6d35f17b457396bf00e8d00d

Source range

937:0–939:8

Open exact source occurrence

Indexed statement

∀ {α : Type u_2} {β : Type u_3} [inst : Preorder.{u_2} α] [inst_1 : Preorder.{u_3} β] {a₁ a₂ : α} {b₁ b₂ : β},
  Iff
    (@LT.lt.{max u_2 u_3} (Prod.{u_2, u_3} α β)
      (@Preorder.toLT.{max u_2 u_3} (Prod.{u_2, u_3} α β) (@Prod.instPreorder.{u_2, u_3} α β inst inst_1))
      (@Prod.mk.{u_2, u_3} α β a₁ b₁) (@Prod.mk.{u_2, u_3} α β a₂ b₂))
    (Or
      (And (@LT.lt.{u_2} α (@Preorder.toLT.{u_2} α inst) a₁ a₂) (@LE.le.{u_3} β (@Preorder.toLE.{u_3} β inst_1) b₁ b₂))
      (And (@LE.le.{u_2} α (@Preorder.toLE.{u_2} α inst) a₁ a₂) (@LT.lt.{u_3} β (@Preorder.toLT.{u_3} β inst_1) b₁ b₂)))

This text is bound to the statement digest above. Parsing and indexing it does not establish proof validity, informal fidelity, implication or equivalence.

Independent status axes

Source status

SOURCE_INDEXED

Independent verification

NOT_CHECKED

Current applicability

NOT_CHECKED

Freshness

PINNED_HISTORICAL_SOURCE

Action authorization

NONE

Lifecycle and research maturity are UNKNOWN in this source catalogue. The source pin is historical; absence of a newer change or revocation has not been checked.

Declared structural neighborhood

1 incoming and 1 outgoing relations occur in the bounded projection below. DECLARES, IMPORTS_MODULE and TYPE_REFERENCES are structural source relations only. Each explicitly sets logical implication and semantic equivalence to false.

Omitted structural references

• And — named target outside this selected catalogue slice
• Iff — named target outside this selected catalogue slice
• LE.le — named target outside this selected catalogue slice
• LT.lt — named target outside this selected catalogue slice
• Or — named target outside this selected catalogue slice
• Preorder — named target outside this selected catalogue slice
• Preorder.toLE — named target outside this selected catalogue slice
• Preorder.toLT — named target outside this selected catalogue slice
• Prod — named target outside this selected catalogue slice
• Prod.mk — named target outside this selected catalogue slice

Module declarations omitted

148

Module imports omitted

12

Module type references omitted

1687

Omissions are preserved rather than converted into absent relations. Out-of-slice targets remain unsupported by this projection.

Independent validation

Validate the committed catalogue, pins, canonical encoding, identities, relation endpoints, named omissions and authority ceiling from a clean checkout:

python3 -I -S -B conformance/source_catalogue_v1/consumer.py \
  --catalogue-root website/public/catalogues/mathlib/v4.34.1 \
  --policy conformance/source_catalogue_v1/trust-policy.json \
  --policy-sha256 c3cdec2b2c784728621bb8c25a055a1e73d67d3c1c922b7ab62b09003399e1c9 \
  --audit-imports

Manifest · Module shard · Search export

This replay does not fetch Mathlib, rerun Lean, authenticate GitHub, check current applicability, or grant action authority. It validates the pinned publication contract and returns only its bounded source-indexing result.