Theorems · Theorem · order theory
InfClosed.sInf_mem_of_nonempty
∀ {α : Type u_3} [inst : ConditionallyCompleteLattice α] {s t : Set α},
InfClosed s → t.Finite → t.Nonempty → t ⊆ s → sInf t ∈ s- Defined in
- Mathlib.Order.SupClosed
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ConditionallyCompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Elemproof · cited by 7,166
- Finiteproof · cited by 3,029
- Set.Nonemptystatement and proof · cited by 2,627
- Set.Finitestatement and proof · cited by 1,814
- InfSet.sInfstatement · cited by 935
- ConditionallyCompleteLatticestatement and proof · cited by 364
- InfClosedstatement and proof · cited by 57
- Set.Nonempty.to_subtypeproof · cited by 55
- Set.Finite.to_subtypeproof · cited by 44
- sInf_eq_iInf'proof · cited by 17
- InfClosed.iInf_mem_of_nonemptyproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- InfClosed.biInf_mem_of_nonemptyproof · cited by 1