coe_finset_sup — Mathlib

English

For a Finset s of indices and a family U of clopen α, the underlying set of the Finset-sup is the union of the corresponding clopen sets: ↑(s.sup U) = ⋃ i ∈ s, U(i).

Русский

Для конечного множества индексов s и семейства U из клопных множеств α, базовое множество sup по s равно объединению всех U(i) по i ∈ s.

LaTeX

$$$\uparrow (s \sup U) = \bigcup_{i \in s} U(i) \quad (s: \mathrm{Finset}\,\iota,\ U: \iota \to \mathrm{Clopens}(\alpha)).$$$

Lean4

@[simp]
theorem coe_finset_sup (s : Finset ι) (U : ι → Clopens α) : (↑(s.sup U) : Set α) = ⋃ i ∈ s, U i := by
  classical
    induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ _ IH => simp [IH]

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