isOpenMap_sum — Mathlib

English

A map on a sum is open if and only if its projections to each summand are open maps.

Русский

Отображение на сумме открыто тогда, когда проекции на каждую компоненту являются открытыми отображениями.

LaTeX

$$$$\\mathrm{IsOpenMap}(f) \\iff \\Big( \\mathrm{IsOpenMap}(a \\mapsto f(\\mathrm{Sum.inl} a)) \\Big) \\land \\mathrm{IsOpenMap}(b \\mapsto f(\\mathrm{Sum.inr} b)).$$$$

Lean4

theorem isOpenMap_sum {f : X ⊕ Y → Z} : IsOpenMap f ↔ (IsOpenMap fun a => f (inl a)) ∧ IsOpenMap fun b => f (inr b) :=
  by simp only [isOpenMap_iff_nhds_le, Sum.forall, nhds_inl, nhds_inr, Filter.map_map, comp_def]

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