setCongr — Mathlib

English

If two sets are equal, then they are uniformly equivalent as subspaces with the induced uniform structure.

Русский

Если два множества равны, то они равномерно эквивалентны как подпространства с индуцированной равномерной структурой.

LaTeX

$${s t : Set α} (h : s = t) : s ≃ᵤ t$$

Lean4

/-- If two sets are equal, then they are uniformly equivalent. -/
def setCongr {s t : Set α} (h : s = t) : s ≃ᵤ t
    where
  uniformContinuous_toFun := uniformContinuous_subtype_val.subtype_mk _
  uniformContinuous_invFun := uniformContinuous_subtype_val.subtype_mk _
  toEquiv := Equiv.setCongr h

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