subset

Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

URI: https://scilib.ai/kg/mathlib#Coplanar.subset

← MathLib Explorer

English

A subset of a coplanar set is coplanar.

Русский

Подмножество копланарного множества копланарно.

LaTeX

$$Subset ⊆ Coplanar → Coplanar$$

Lean4

/-- A subset of a coplanar set is coplanar. -/
theorem subset {s₁ s₂ : Set P} (hs : s₁ ⊆ s₂) (h : Coplanar k s₂) : Coplanar k s₁ :=
  (Submodule.rank_mono (vectorSpan_mono k hs)).trans h

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

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

Разделы

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

Аффилиация

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