mk'_top

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

English

The construction mk' p ⊤ yields the whole space.

Русский

Конструкция mk' p ⊤ даёт всё пространство.

LaTeX

$$$\\mathrm{mk}'(p,\\top) = \\top$$$

Lean4

@[simp]
theorem mk'_top (p : P) : mk' p (⊤ : Submodule k V) = ⊤ :=
  by
  ext x
  simp [mem_mk']

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

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

Разделы

Аффилиация

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