separationQuotient_iff — Mathlib

English

IsUltraUniformity(SeparationQuotient X) if and only if IsUltraUniformity X.

Русский

IsUltraUniformity(SeparationQuotient X) тогда и только тогда, когда IsUltraUniformity X.

LaTeX

$$$IsUltraUniformity\big(SeparationQuotient X\big) \iff IsUltraUniformity(X)$$$

Lean4

@[simp]
theorem separationQuotient_iff : IsUltraUniformity (SeparationQuotient X) ↔ IsUltraUniformity X :=
  ⟨fun _ ↦ SeparationQuotient.isUniformInducing_mk.isUltraUniformity, fun _ ↦ inferInstance⟩

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