ext_linear_iff — Mathlib

English

The constructed affine map mk' from f, f', p, h has linear part equal to f'.

Русский

Сконструированное отображение mk' из f, f', p, h имеет линейную часть, равную f'.

LaTeX

$$mk' f f' p h .linear = f'$$

Lean4

/-- Two affine maps are equal if they have equal linear maps and are equal at some point. -/
theorem ext_linear_iff {f g : P1 →ᵃ[k] P2} : f = g ↔ (f.linear = g.linear) ∧ (∃ p, f p = g p) :=
  ⟨fun h ↦ ⟨congrArg _ h, by inhabit P1; exact default, by rw [h]⟩, fun h ↦
    Exists.casesOn h.2 fun _ hp ↦ ext_linear h.1 hp⟩

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