contLinear_eq_zero_iff_exists_const

English

Equivalent formulation: contLinear being zero implies existence of a constant affine map and conversely.

Русский

Эквивалентная формулировка: contLinear = 0 эквивалентно существованию константной аффинной карты и наоборот.

LaTeX

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

Lean4

theorem contLinear_eq_zero_iff_exists_const (f : P →ᴬ[R] Q) : f.contLinear = 0 ↔ ∃ q, f = const R P q :=
  by
  have h₁ : f.contLinear = 0 ↔ (f : P →ᵃ[R] Q).linear = 0 :=
    by
    refine ⟨fun h => ?_, fun h => ?_⟩ <;> ext
    · rw [← coe_contLinear_eq_linear, h]; rfl
    · rw [← coe_linear_eq_coe_contLinear, h]; rfl
  have h₂ : ∀ q : Q, f = const R P q ↔ (f : P →ᵃ[R] Q) = AffineMap.const R P q :=
    by
    intro q
    refine ⟨fun h => ?_, fun h => ?_⟩ <;> ext
    · rw [h]; rfl
    · rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]
  simp_rw [h₁, h₂]
  exact (f : P →ᵃ[R] Q).linear_eq_zero_iff_exists_const

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