wellFoundedGT_characterisations — Mathlib

English

A collection of tenets equating WellFoundedGT with various compactness properties in a complete lattice.

Русский

Комплекс условий, показывающий эквивалентность WellFoundedGT и различных свойств компактности в полной решётке.

LaTeX

$$List.TFAE [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ k : α, IsCompactElement k]$$

Lean4

theorem wellFoundedGT_characterisations :
    List.TFAE [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ k : α, IsCompactElement k] :=
  by
  tfae_have 1 → 2 := @WellFoundedGT.isSupFiniteCompact α _
  tfae_have 2 → 3 := IsSupFiniteCompact.isSupClosedCompact α
  tfae_have 3 → 1 := IsSupClosedCompact.wellFoundedGT α
  tfae_have 2 ↔ 4 := isSupFiniteCompact_iff_all_elements_compact α
  tfae_finish

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