replaceBornology_eq — Mathlib

English

If the supplied equivalence of bounded sets holds, then replacing the bornology yields back the original space: m.replaceBornology H = m.

Русский

Если эквивалентность ограниченных множеств выполняется, то замена Bornology возвращает исходное пространство: m.replaceBornology H = m.

LaTeX

$$$m.replaceBornology\\ H = m$ when $H$ encodes the same boundedness relation as the original bornology.$$

Lean4

theorem replaceBornology_eq {α} [m : PseudoMetricSpace α] [B : Bornology α]
    (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
    PseudoMetricSpace.replaceBornology _ H = m := by
  ext
  rfl
    -- ensure that the uniformity is unchanged when replacing the bornology.

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