coe_finset_sup — Mathlib

English

For a finitary indexed family of opens, the underlying set of the Finset-sup equals the Finset-sup of the underlying sets.

Русский

Для конечной семейной индексации открытых множеств их конечный суп по основаниям имеет основание над множество открытых множеств.

LaTeX

$$$ (↑(s.sup f) : Set α) = s.sup ((↑) \circ f) $$$

Lean4

@[simp, norm_cast]
theorem coe_finset_sup (f : ι → Opens α) (s : Finset ι) : (↑(s.sup f) : Set α) = s.sup ((↑) ∘ f) :=
  map_finset_sup (⟨⟨(↑), coe_sup⟩, coe_bot⟩ : SupBotHom (Opens α) (Set α)) _ _

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