le_iff_compact_le_imp — Mathlib

English

For compactly generated lattices and a, b ∈ α, a ≤ b iff every compact c ≤ a also ≤ b.

Русский

Для компактно сгенерируемых решёток и элементов a, b: a ≤ b тогда и только тогда, когда для каждого компактного c: c ≤ a ⇒ c ≤ b.

LaTeX

$$le_iff_compact_le_imp$$

Lean4

theorem le_iff_compact_le_imp {a b : α} : a ≤ b ↔ ∀ c : α, CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b :=
  ⟨fun ab _ _ ca => le_trans ca ab, fun h =>
    by
    rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]
    exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩⟩

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