sup_mem — Mathlib

English

If a set s is closed under bottom and closed under binary join, then the finite supremum of any finite family of elements of a set s is again in s.

Русский

Если s содержит ⊥ и закрыто относительно взятия объединения двух элементов, то для любой конечнойFamily элементов из s их супремум принадлежит s.

LaTeX

$$$(\forall i \in t, p i \in s) \Rightarrow t.sup p ∈ s$$$

Lean4

theorem sup_mem (s : Set α) (w₁ : ⊥ ∈ s) (w₂ : ∀ᵉ (x ∈ s) (y ∈ s), x ⊔ y ∈ s) {ι : Type*} (t : Finset ι) (p : ι → α)
    (h : ∀ i ∈ t, p i ∈ s) : t.sup p ∈ s :=
  @sup_induction _ _ _ _ _ _ (· ∈ s) w₁ w₂ h

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