instRespectsIsoW — Mathlib

English

W respects isomorphisms: pre- and post-composition with iso preserves membership in W.

Русский

W сохраняет изоморфизмы: левые и правые композиции с изоморфизмами сохраняют принадлежность к W.

LaTeX

$$$W \\text{ .RespectsIso}$$$

Lean4

instance : (W P).RespectsIso
    where
  precomp f (_ : IsIso f) g hg := (W P).comp_mem f g (W_of_isIso _ f) hg
  postcomp f (_ : IsIso f) g hg := (W P).comp_mem g f hg (W_of_isIso _ f)

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