coe_finset_inf — Mathlib

English

For a Finset s and family f, the underlying set of s.inf f equals the infimum of the underlying sets.

Русский

Для Finset s и семейства(f) соответствующее множество пересечения открытых множеств равно пересечению соответствующих множеств.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_finset_inf (f : ι → Opens α) (s : Finset ι) : (↑(s.inf f) : Set α) = s.inf ((↑) ∘ f) :=
  map_finset_inf (⟨⟨(↑), coe_inf⟩, coe_top⟩ : InfTopHom (Opens α) (Set α)) _ _

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