coe_linear_eq_coe_contLinear — Mathlib

English

A continuous affine map has zero contLinear if and only if it is constant; i.e., f.contLinear = 0 ⇔ ∃ q, f = const R P q.

Русский

Континуальная линейная часть равна нулю тогда и только тогда, когда карта константна; т.е. f.contLinear = 0 ⇔ ∃ q, f = const R P q.

LaTeX

$$$f.contLinear = 0 \iff \exists q,\ f = const R P q$$$

Lean4

theorem coe_linear_eq_coe_contLinear (f : P →ᴬ[R] Q) : ((f : P →ᵃ[R] Q).linear : V → W) = (⇑f.contLinear : V → W) :=
  rfl

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