instIsCompactlyGenerated — Mathlib

English

Let α be a complete lattice and suppose α is compactly generated. Then for every a ∈ α, the interval Iic(a) is also compactly generated.

Русский

Пусть α — полная решетка и α компактно порождается. Тогда для каждого a ∈ α интервал Iic(a) также компактно порожден.

LaTeX

$$$IsCompactlyGenerated(Iic(a))$$$

Lean4

instance instIsCompactlyGenerated [IsCompactlyGenerated α] {a : α} : IsCompactlyGenerated (Iic a) :=
  by
  refine ⟨fun ⟨x, (hx : x ≤ a)⟩ ↦ ?_⟩
  obtain ⟨s, hs, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq x
  rw [sSup_le_iff] at hx
  let f : s → Iic a := fun y ↦ ⟨y, hx _ y.property⟩
  refine ⟨range f, ?_, ?_⟩
  · rintro - ⟨⟨y, hy⟩, hy', rfl⟩
    exact isCompactElement (hs _ hy)
  · rw [Subtype.ext_iff]
    change sSup (((↑) : Iic a → α) '' (range f)) = sSup s
    congr
    ext b
    simpa [f] using hx b

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