orthogonalProjectionFn_mem_orthogonal

English

The element orthogonalProjectionFn s p lies in mk' p s.direction.orthogonal.

Русский

Элемент orthogonalProjectionFn s p лежит в mk' p s.direction.orthogonal.

LaTeX

$$orthogonalProjectionFn s p ∈ mk' p s.direction.orthogonal$$

Lean4

/-- The `orthogonalProjectionFn` lies in the orthogonal
subspace. This lemma is only intended for use in setting up the
bundled version and should not be used once that is defined. -/
theorem orthogonalProjectionFn_mem_orthogonal {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] (p : P) : orthogonalProjectionFn s p ∈ mk' p s.directionᗮ :=
  by
  rw [← mem_coe, ← Set.singleton_subset_iff, ← inter_eq_singleton_orthogonalProjectionFn]
  exact Set.inter_subset_right

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