interior_pi_set — Mathlib

English

The interior of a Pi-set over a finite index is the Pi of interiors.

Русский

interior (pi I s) = I.pi interior(s(i)) для конечного I.

LaTeX

$$$\\displaystyle \\operatorname{interior}\\bigl( \\pi I s \\bigr) = I .\\pi\\bigl( \\lambda i . \\operatorname{interior}(s(i)) \\bigr).$$$

Lean4

theorem interior_pi_set {I : Set ι} (hI : I.Finite) {s : ∀ i, Set (A i)} :
    interior (pi I s) = I.pi fun i => interior (s i) := by
  ext a
  simp only [Set.mem_pi, mem_interior_iff_mem_nhds, set_pi_mem_nhds_iff hI]

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