preimage_iSup_eq_top — Mathlib

English

If the supremum of opens U_i in Y is the top open, then the supremum of their preimages under f is also the top open.

Русский

Если верхний предел открытий U_i в Y равен верхнему открытому, то и верхний предел их прообразов под f равен верхнему открытому.

LaTeX

$$$\\bigvee_i f^{-1}ᵁ U_i = \\top$$$

Lean4

theorem preimage_iSup_eq_top {ι} {U : ι → Opens Y} (hU : iSup U = ⊤) : ⨆ i, f ⁻¹ᵁ U i = ⊤ :=
  f.preimage_iSup U ▸ hU ▸ rfl

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