finsetSup_mem — Mathlib

English

If hC is a SetRing and the members s(i) ∈ C for i in a finite index set t, then t.sup s ∈ C.

Русский

Если hC — кольцо множеств и для каждого i в t выполняется s(i) ∈ C, то t.sup s ∈ C.

LaTeX

$$$\text{If } hC\text{ is SetRing } hs: \forall i\in t, s(i)\in C, \text{ then } t\,\mathrm{sup}\,s \in C.$$$

Lean4

theorem finsetSup_mem (hC : IsSetRing C) {ι : Type*} {s : ι → Set α} {t : Finset ι} (hs : ∀ i ∈ t, s i ∈ C) :
    t.sup s ∈ C := by
  classical
    induction t using Finset.induction_on with
  | empty => exact hC.empty_mem
  | insert m t hm ih =>
    simpa only [sup_insert] using
      hC.union_mem (hs m <| mem_insert_self m t) (ih <| fun i hi ↦ hs _ <| mem_insert_of_mem hi)

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