self_mem_mk'

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#AffineSubspace.self_mem_mk'

← MathLib Explorer

English

The base point lies in the constructed affine subspace mk' p direction.

Русский

Базовая точка принадлежит mk' p direction.

LaTeX

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

Lean4

/-- An affine subspace constructed from a point and a direction contains that point. -/
theorem self_mem_mk' (p : P) (direction : Submodule k V) : p ∈ mk' p direction := by simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru