mk' — Mathlib

English

The direction of the affine subspace mk'(p, D) equals D.

Русский

Направление подпространства mk'(p, D) равно D.

LaTeX

$$$\\text{mk}'(p, D).direction = D$$$

Lean4

/-- Construct an affine subspace from a point and a direction. -/
def mk' (p : P) (direction : Submodule k V) : AffineSubspace k P
    where
  carrier := {q | q -ᵥ p ∈ direction}
  smul_vsub_vadd_mem c p₁ p₂ p₃ hp₁ hp₂
    hp₃ := by simpa [vadd_vsub_assoc] using direction.add_mem (direction.smul_mem c (direction.sub_mem hp₁ hp₂)) hp₃

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