Theorems · Theorem · order theory
SetLike.lt_iff_le_and_exists
∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : PartialOrder A] [IsConcreteLE A B] {p q : A},
p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p- Defined in
- Mathlib.Data.SetLike.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- SetLikestatement and proof · cited by 1,084
- lt_iff_le_not_geproof · cited by 35
- IsConcreteLEstatement and proof · cited by 28
- SetLike.not_le_iff_existsproof · cited by 10
Cited by14
Results whose statement or proof uses this declaration.
- Ring.krullDimLE_zero_and_isLocalRing_tfaeproof · cited by 7
- Ideal.height_le_spanRank_toENat_of_mem_minimalPrimesproof · cited by 5
- Ideal.isMaximal_of_isIntegral_of_isMaximal_comapproof · cited by 5
- Ideal.IsIntegral.comap_lt_comapproof · cited by 3
- LocalSubring.exists_valuationRing_of_isMaxproof · cited by 2
- Ideal.exist_integer_multiples_notMemproof · cited by 1
- AffineSubspace.sup_direction_lt_of_nonempty_of_inter_emptyproof · cited by 1
- Ideal.comap_lt_comap_of_root_mem_sdiffproof · cited by 1
- Subgroup.relIndex_strictPeriodsproof · cited by 1
- Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisorsproof · cited by 1
- AffineSubspace.direction_lt_of_nonemptyproof · cited by 1