linear_eq_zero_iff_exists_const — Mathlib

English

There always exist affine maps between any two affine spaces P1 and P2, i.e., the type of affine maps P1 →ᵃ[k] P2 is nonempty.

Русский

Всегда существует как минимум одно аффинное отображение между любыми двумя аффинными пространствами P1 и P2.

LaTeX

$$Nonempty (P1 →ᵃ[k] P2)$$

Lean4

theorem linear_eq_zero_iff_exists_const (f : P1 →ᵃ[k] P2) : f.linear = 0 ↔ ∃ q, f = const k P1 q :=
  by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · use f (Classical.arbitrary P1)
    ext
    rw [coe_const, Function.const_apply, ← @vsub_eq_zero_iff_eq V2, ← f.linearMap_vsub, h, LinearMap.zero_apply]
  · rcases h with ⟨q, rfl⟩
    exact const_linear k P1 q

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