setoid — Mathlib

English

There is a setoid on NonemptyCompacts ℓ_∞(ℝ) identifying two nonempty compact subspaces if they are isometric.

Русский

Существует сетойд на множестве не пустых компактных подпространств ℓ∞(ℝ), идентифицирующий две не пустые компактные подмножества, если они изометричны.

LaTeX

$$Setoid (NonemptyCompacts ℓ_infty_ℝ) := IsometryRel equivalence_isometryRel$$

Lean4

/-- setoid instance identifying two isometric nonempty compact subspaces of ℓ^∞(ℝ) -/
instance setoid : Setoid (NonemptyCompacts ℓ_infty_ℝ) :=
  Setoid.mk IsometryRel equivalence_isometryRel

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