instHasOfPrecompPropertyIsomorphismsOfRespectsIso

English

If W has the Isomorphisms structure and W is separable under precomposition, then W.HasOfPrecompProperty is inherited by isomorphisms.

Русский

Если W удовлетворяет структурe Изоморфизмов и сохраняется по префиксному компоненту, то для изоморфизмов выполняется свойство HasOfPrecompProperty.

LaTeX

$$$ [W.\\text{RespectsIso}] \\Rightarrow W.HasOfPrecompProperty (\\text{isomorphisms } C).$$$

Lean4

instance [W.RespectsIso] : W.HasOfPrecompProperty (isomorphisms C) where
  of_precomp _ _ (_ : IsIso _) := (W.cancel_left_of_respectsIso _ _).mp

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