MathGraph.

← Search the knowledge catalogue · Qualified object projection

Mathlib source occurrence

le_of_forall_gt_imp_ge_of_dense

A source-pinned catalogue entry. MathGraph indexed these exact bytes and structural references; it did not independently check this declaration as a proof.

SOURCE_INDEXED · independent verification NOT_CHECKED · authority NONE

Exact source identity

Canonical occurrence
object-ff799edb267b87ec1627946823ee09bf33eac4f544c489b0b2c56f8ba79fcfc3
Kind
theorem
Module
Mathlib.Order.Basic
Path
Mathlib/Order/Basic.lean
Commit
d13f23b723b8a846827a245b89c10fc7d3f11612
Tree
efa132418a56d0e38c56cc412a06df22178dac5c
Statement digest
57d49a95575660981da12064379c298b649e3dd4dbc0fcb94b0b6f6e014a16bc
Source range
1021:0–1025:69

Open exact source occurrence

Indexed statement

∀ {α : Type u_2} [inst : LinearOrder.{u_2} α]
  [@DenselyOrdered.{u_2} α
      (@Preorder.toLT.{u_2} α (@PartialOrder.toPreorder.{u_2} α (@LinearOrder.toPartialOrder.{u_2} α inst)))]
  {a₁ a₂ : α},
  (∀ (a : α),
      @LT.lt.{u_2} α
          (@Preorder.toLT.{u_2} α (@PartialOrder.toPreorder.{u_2} α (@LinearOrder.toPartialOrder.{u_2} α inst))) a₂ a →
        @LE.le.{u_2} α
          (@Preorder.toLE.{u_2} α (@PartialOrder.toPreorder.{u_2} α (@LinearOrder.toPartialOrder.{u_2} α inst))) a₁ a) →
    @LE.le.{u_2} α
      (@Preorder.toLE.{u_2} α (@PartialOrder.toPreorder.{u_2} α (@LinearOrder.toPartialOrder.{u_2} α inst))) a₁ a₂

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

  • LE.le — named target outside this selected catalogue slice
  • LT.lt — named target outside this selected catalogue slice
  • LinearOrder — named target outside this selected catalogue slice
  • LinearOrder.toPartialOrder — named target outside this selected catalogue slice
  • PartialOrder.toPreorder — 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
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.

Bounded source neighborhood

Navigate exact declared source structure around this occurrence. The projection is capped at 8 objects and 12 relations; named omissions and out-of-slice references stay visible above.

Declared objects and relations

Presentation projection · authority NONE · not a certificate, proof, or verifier

Position and proximity organize this view only. Every arrow repeats an exact structural relation whose logical implication and semantic equivalence flags are false.

Filter declared relation types

3 of 3 objects · 3 of 3 relations · omitted: 0 objects, 0 relations

This page is capped at 8 objects and 12 relations. Counts preserve the complete one-hop selected scope, including named omissions.

Incoming

Selected occurrence

Outgoing

Display-only traversal

Follow only the currently displayed declared arrows. This is not proof search, verification or support closure.

No traversal requested.

    Declared relation list

    1. le_of_forall_gt_imp_ge_of_denseTYPE_REFERENCESDenselyOrdereddirected · implication false · equivalence false · authority NONE
    2. Mathlib.Order.BasicDECLARESle_of_forall_gt_imp_ge_of_densedirected · implication false · equivalence false · authority NONE
    3. Mathlib.Order.BasicDECLARESDenselyOrdereddirected · implication false · equivalence false · authority NONE

    Visual projection

    The diagram is drawn from the same bounded payload after JavaScript loads. The semantic lists remain the accessible source of exact links and relation labels.

    Enable JavaScript to draw the visual projection.

    Download displayed subgraph

    Export kind PRESENTATION_PROJECTION · authority NONE · semantics READ_ONLY_SOURCE_STRUCTURE. It is not an evidence receipt and grants no action authority.