Theorems · Theorem · order theory
OrderEmbedding.le_iff_le
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α}, f a ≤ f b ↔ a ≤ b- Defined in
- Mathlib.Order.Hom.Basic
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Preorderstatement and proof · cited by 7,952
- OrderEmbeddingstatement and proof · cited by 619
- RelEmbedding.map_rel_iffproof · cited by 25
Cited by32
Results whose statement or proof uses this declaration.
- Rat.cast_leproof · cited by 9
- IsLocalization.isPrime_iff_isPrime_disjointproof · cited by 6
- NNRat.cast_leproof · cited by 4
- InitialSeg.le_iff_leproof · cited by 4
- OrderEmbedding.preimage_Iciproof · cited by 3
- OrderEmbedding.preimage_Iicproof · cited by 3
- Disjoint.of_orderEmbeddingproof · cited by 3
- CategoryTheory.CardinalDirectedPoset.Hom.le_iff_leproof · cited by 2
- IsLocalization.under_le_under_iffproof · cited by 2
- Ordinal.preOmega_le_preOmegaproof · cited by 2
- SimpleGraph.disjoint_edgeSetproof · cited by 2
- Ordinal.omega_le_omegaproof · cited by 1