ext_iff

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#AffineSubspace.ext_iff

English

Two affine subspaces are equal if and only if their underlying sets of points are equal.

Русский

Два афинных подпространства равны тогда и только тогда, когда совпадают их множества точек.

LaTeX

$$$s_1 = s_2 \\iff (s_1 : Set\\ P) = (s_2 : Set\\ P)$$$

Lean4

protected theorem ext_iff (s₁ s₂ : AffineSubspace k P) : s₁ = s₂ ↔ (s₁ : Set P) = s₂ :=
  SetLike.ext'_iff

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

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

Разделы

Аффилиация

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