swap — Mathlib

English

If f,g is reflexive, then g,f is reflexive.

Русский

Если f,g — рефлексивная пара, то g,f тоже рефлексивна.

LaTeX

$$$\text{If } \text{IsReflexivePair}(f,g) \Rightarrow \text{IsReflexivePair}(g,f)$$$

Lean4

/-- If `f,g` is reflexive, then `g,f` is reflexive. -/
theorem swap [IsReflexivePair f g] : IsReflexivePair g f :=
  IsReflexivePair.mk' _ (section_comp_right f g)
    (section_comp_left f g)
      -- This shouldn't be an instance as it would instantly loop.

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