symm — Mathlib

English

The relation Rel' is symmetric: if x is related to y, then y is related to x, by cases on the sum type.

Русский

Отношение Rel' симметрично: если x связано с y, то y связано с x, рассуждая по случаям на сумма-типе.

LaTeX

$$Rel'(f,g) x y → Rel'(f,g) y x$$

Lean4

theorem symm {x y : X₁ ⊕ X₂} (h : Rel' f g x y) : Rel' f g y x :=
  by
  obtain _ | ⟨_, _, h⟩ | _ | _ := h
  · apply Rel'.refl
  · exact Rel'.inl_inl _ _ h.symm
  · exact Rel'.inr_inl _
  · exact Rel'.inl_inr _

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