lineMap_continuous — Mathlib

English

Equivalent reformulations show that the openness of the linear part corresponds to openness of the affine map itself.

Русский

Эквивалентные формулировки показывают, что открытость линейной части соответствует открытости самого афинного отображения.

LaTeX

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

Lean4

/-- The line map is continuous. -/
@[continuity, fun_prop]
theorem lineMap_continuous {p q : P} : Continuous (lineMap p q : R →ᵃ[R] P) :=
  by
  rw [coe_lineMap]
  fun_prop

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