sup'_mem — Mathlib

English

If s is a set in α closed under sup and t is nonempty with p: t → α such that p(i) ∈ s for all i ∈ t, then t.sup' H p ∈ s.

Русский

Если s замкнуто относительно объединения и т не пустое, и p(i) ∈ s для всех i ∈ t, то t.sup' H p ∈ s.

LaTeX

$$$t.sup' H p \in s$$$

Lean4

theorem sup'_mem (s : Set α) (w : ∀ᵉ (x ∈ s) (y ∈ s), x ⊔ y ∈ s) {ι : Type*} (t : Finset ι) (H : t.Nonempty) (p : ι → α)
    (h : ∀ i ∈ t, p i ∈ s) : t.sup' H p ∈ s :=
  sup'_induction H p w h

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