isOpenMap_linear_iff — Mathlib

English

For an affine map f, the linear part f.linear is an open map if and only if f is an open map.

Русский

Для аффинного отображения f линейная часть f.linear является открытым отображением тогда и только тогда, когда само отображение f открыто.

LaTeX

$$$IsOpenMap(f.linear) \iff IsOpenMap(f)$$$

Lean4

/-- If `f` is an affine map, then its linear part is an open map iff `f` is an open map. -/
theorem isOpenMap_linear_iff {f : P →ᵃ[R] Q} : IsOpenMap f.linear ↔ IsOpenMap f :=
  by
  inhabit P
  have : (f.linear : V → W) = (Homeomorph.vaddConst <| f default).symm ∘ f ∘ (Homeomorph.vaddConst default) :=
    by
    ext v
    simp
  rw [this]
  simp only [Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff']

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