replaceBornology_eq — Mathlib

English

If the boundedness relation is preserved under replacement, the resulting space equals the original.

Русский

Если отношение ограниченности сохраняется при замене, полученное пространство равно исходному.

LaTeX

$$MetricSpace.replaceBornology _ H = m$$

Lean4

theorem replaceBornology_eq {α} [m : MetricSpace α] [B : Bornology α]
    (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) : MetricSpace.replaceBornology _ H = m :=
  by
  ext
  rfl

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