continuous_iff — Mathlib

English

An affine map is continuous if and only if its underlying linear map is continuous.

Русский

Аффинное отображение непрерывно тогда и только тогда, когда непрерывна его линейная часть.

LaTeX

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

Lean4

/-- An affine map is continuous iff its underlying linear map is continuous. See also
`AffineMap.continuous_linear_iff`. -/
@[deprecated continuous_linear_iff (since := "2025-09-13")]
theorem continuous_iff {f : P →ᵃ[R] Q} : Continuous f ↔ Continuous f.linear :=
  continuous_linear_iff.symm

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