Theorems · Theorem · order theory
CompleteLattice.Iic_coatomic_of_compact_element
∀ {α : Type u_2} [inst : CompleteLattice α] {k : α}, IsCompactElement k → IsCoatomic ↑(Set.Iic k)A compact element k has the property that any b < k lies below a "maximal element below
k", which is to say [⊥, k] is coatomic.
- Defined in
- Mathlib.Order.CompactlyGenerated.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
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
- Top.topproof · cited by 9,680
- Set.Elemstatement and proof · cited by 7,166
- Set.Nonemptyproof · cited by 2,627
- LT.lt.leproof · cited by 2,189
- le_of_ltproof · cited by 1,175
- Set.Iioproof · cited by 1,166
- eq_or_neproof · cited by 1,117
- Set.Iicstatement and proof · cited by 1,111
- CompleteLatticestatement and proof · cited by 1,048
- SupSet.sSupproof · cited by 954
- lt_of_le_of_neproof · cited by 230
Cited by1
Results whose statement or proof uses this declaration.
- CompleteLattice.coatomic_of_top_compactproof · cited by 0