isCompactlyGenerated_of_wellFoundedGT

English

If α is a complete lattice with a well-founded greater-than relation, then α is compactly generated.

Русский

Если α — полная решётка с хорошо упорядоченным отношением больше, то α компактно порождается.

LaTeX

$$$ \text{WellFoundedGT}(\alpha) \Rightarrow \text{IsCompactlyGenerated}(\alpha) $$$

Lean4

theorem isCompactlyGenerated_of_wellFoundedGT [h : WellFoundedGT α] : IsCompactlyGenerated α :=
  by
  rw [wellFoundedGT_iff_isSupFiniteCompact, isSupFiniteCompact_iff_all_elements_compact] at h
  exact ⟨fun x => ⟨{ x }, ⟨fun x _ => h x, sSup_singleton⟩⟩⟩

Похожие утверждения