ext — Mathlib

English

Extensionality principle for affine subspaces: equality is determined by membership of all points.

Русский

Принцип экстензии для аффинных подпространств: равенство определяется принадлежностью всех точек.

LaTeX

$$$\\forall p,q:\\ AffineSubspace k P, (\\forall x, x \\in p \\iff x \\in q) \\Rightarrow p = q$$$

Lean4

@[ext (iff := false)]
theorem ext {p q : AffineSubspace k P} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q :=
  SetLike.ext h

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