equiv_trans — Mathlib

English

For Homeomorph f : α ≃ₜ β and g : β ≃ₜ γ, Compacts.equiv (f.trans g) equals (Compacts.equiv f).trans (Compacts.equiv g).

Русский

Для гомеоморфизмов f : α ≃ₜ β и g : β ≃ₜ γ эквиваленция Compacts удовлетворяет: Compacts.equiv (f.trans g) = (Compacts.equiv f).trans (Compacts.equiv g).

LaTeX

$$$\\forall {f : \\alpha \\equiv_{\\mathrm{t}} \\beta} {g : \\beta \\equiv_{\\mathrm{t}} \\gamma},\\\\ Compacts.equiv (f.trans g) = (Compacts.equiv f).trans (Compacts.equiv g)$$$

Lean4

@[simp]
theorem equiv_trans (f : α ≃ₜ β) (g : β ≃ₜ γ) :
    Compacts.equiv (f.trans g) = (Compacts.equiv f).trans (Compacts.equiv g) :=
  Equiv.ext <| map_comp g f g.continuous f.continuous

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