continuous_linear_iff — Mathlib

English

For an affine map f: P →ᵃ[R] Q, the linear part f.linear is continuous if and only if f is continuous.

Русский

Для аффинного отображения f: P →ᵃ[R] Q линейная часть f.linear непрерывна тогда и только тогда, когда само отображение f непрерывно.

LaTeX

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

Lean4

/-- If `f` is an affine map, then its linear part is continuous iff `f` is continuous. -/
theorem continuous_linear_iff {f : P →ᵃ[R] Q} : Continuous f.linear ↔ Continuous 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_continuous_iff, Homeomorph.comp_continuous_iff']

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