mk'_eq — Mathlib

English

If p ∈ s, mk' p s.direction = s.

Русский

Если p ∈ s, то mk' p s.direction = s.

LaTeX

$$$p \\in s \\Rightarrow \\text{mk}'(p, s.direction) = s$$$

Lean4

/-- Constructing an affine subspace from a point in a subspace and that subspace's direction
yields the original subspace. -/
@[simp]
theorem mk'_eq {s : AffineSubspace k P} {p : P} (hp : p ∈ s) : mk' p s.direction = s :=
  ext_of_direction_eq (direction_mk' p s.direction) ⟨p, Set.mem_inter (self_mem_mk' _ _) hp⟩

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