mk'_nonempty

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

← MathLib Explorer

English

The affine subspace mk' p direction is nonempty.

Русский

Aфинное подпространство mk' p direction непусто.

LaTeX

$$$(\\text{mk}'(p, \\text{direction}) : Set P).Nonempty$$$

Lean4

/-- An affine subspace constructed from a point and a direction is nonempty. -/
theorem mk'_nonempty (p : P) (direction : Submodule k V) : (mk' p direction : Set P).Nonempty :=
  ⟨p, self_mem_mk' p direction⟩

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

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

Разделы

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

Аффилиация

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