Theorems · Theorem · order theory
inf_idem
∀ {α : Type u} [inst : SemilatticeInf α] (a : α), a ⊓ a = a- Defined in
- Mathlib.Order.Lattice
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses propext
- Assumes
- SemilatticeInf
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SemilatticeInfstatement and proof · cited by 634
- inf_of_le_leftproof · cited by 186
- Std.ge_reflproof · cited by 23
Cited by37
Results whose statement or proof uses this declaration.
- sdiff_sdiff_right_selfproof · cited by 20
- sdiff_supproof · cited by 7
- nhdsWithin_interproof · cited by 6
- Function.support_infproof · cited by 4
- nonZeroDivisorsLeft_eq_nonZeroDivisorsproof · cited by 4
- Function.mulSupport_infproof · cited by 3
- inf_inf_distrib_leftproof · cited by 3
- inf_inf_distrib_rightproof · cited by 3
- Submodule.IsPrimary.infproof · cited by 2
- Submodule.rank_sup_add_rank_inf_eqproof · cited by 2
- iSupIndep_iff_supIndepproof · cited by 2
- Filter.Tendsto.min_rightproof · cited by 2