coe_finset_sup — Mathlib

English

For a Finset I and a function f from I to closed sets, the underlying set of the finite sup over I equals the finite sup of the underlying sets.

Русский

Для конечного множества индексов и функции в множество замкнутых подмножеств, множество, соответствующее их конечному объединению, равняется объединению соответствующих множеств.

LaTeX

$$$(s \sup f)^{\uparrow} = s \sup (\uparrow \circ f).$$$

Lean4

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

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