direction_mk' — Mathlib

English

The direction of mk'(p, direction) equals direction.

Русский

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

LaTeX

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

Lean4

/-- The direction of an affine subspace constructed from a point and a direction. -/
@[simp]
theorem direction_mk' (p : P) (direction : Submodule k V) : (mk' p direction).direction = direction :=
  by
  ext v
  rw [mem_direction_iff_eq_vsub (mk'_nonempty _ _)]
  constructor
  · rintro ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    simpa using direction.sub_mem hp₁ hp₂
  · exact fun hv => ⟨v +ᵥ p, vadd_mem_mk' _ hv, p, self_mem_mk' _ _, (vadd_vsub _ _).symm⟩

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