exists_sup_eq_iSup — Mathlib

English

If β is a complete lattice and f: α → β, there exists a finite t ⊆ α such that t.sup f = ⨆ a, f(a).

Русский

Пусть β — полная решетка и f: α → β. Существует конечное множество t ⊆ α такое, что t.sup f = ⨆_{a∈α} f(a).

LaTeX

$$$ \exists t : Finset(\,α\,), t.sup f = \bigvee_{a} f(a) $$$

Lean4

theorem exists_sup_eq_iSup [CompleteLattice β] [WellFoundedGT β] (f : α → β) : ∃ t : Finset α, t.sup f = ⨆ a, f a :=
  have ⟨t, ht⟩ := exists_sup_ge f
  ⟨t, (Finset.sup_le fun _ _ ↦ le_iSup ..).antisymm <| iSup_le ht⟩

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