instHasTwoOutOfThreePropertyW — Mathlib

English

W satisfies the two-out-of-three property: if two out of f, g, and g∘f belong to W, then so does the third.

Русский

W удовлетворяет свойству двух из трёх: если две из f, g, g∘f принадлежат W, то и третья принадлежность выполняется.

LaTeX

$$$W.P.\\HasTwoOutOfThreeProperty$$$

Lean4

instance : (W P).HasTwoOutOfThreeProperty
    where
  of_postcomp f g hg hfg Z
    hZ := by
    rw [← Function.Bijective.of_comp_iff _ (hg Z hZ)]
    simpa using hfg Z hZ
  of_precomp f g hf hfg Z
    hZ := by
    rw [← Function.Bijective.of_comp_iff' (hf Z hZ)]
    simpa using hfg Z hZ

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