mem_carrier_iff

Mathlib.LinearAlgebra.Projectivization.Subspace

URI: https://scilib.ai/kg/mathlib#Projectivization.Subspace.mem_carrier_iff

English

For any subspace A of V and any x in the projective space, x belongs to A if and only if x belongs to A.

Русский

Для любого подпространства A ⊆ V и любого x ∈ ℙ_K V выполняется x ∈ A.carrier тогда и только если x ∈ A.

LaTeX

$$$x \in A.\mathrm{carrier} \iff x \in A$$$

Lean4

@[simp]
theorem mem_carrier_iff (A : Subspace K V) (x : ℙ K V) : x ∈ A.carrier ↔ x ∈ A :=
  Iff.refl _

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

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

Разделы

Аффилиация

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