symm — Mathlib

English

If f is a map with property P, then f is homotopic with itself under P.

Русский

Если f удовлетворяет P, то f гомотопично эквивалентен самому себе по P.

LaTeX

$$HomotopicWith f f P$$

Lean4

@[symm]
theorem symm ⦃f g : C(X, Y)⦄ (h : HomotopicWith f g P) : HomotopicWith g f P :=
  ⟨h.some.symm⟩
    -- Note: this was formerly tagged with `@[trans]`, and although the `trans` attribute accepted it
    -- the `trans` tactic could not use it.
    -- An update to the trans tactic coming in https://github.com/leanprover-community/mathlib4/pull/7014 will reject this attribute.
    -- It could be restored by changing the argument order to `HomotopicWith P f g`.

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