symm_apply_rel — Mathlib

English

For e : r ≃r s, the relation r x (e.symm y) ↔ s (e x) y holds, expressing the compatibility of symmetry with the reliso map.

Русский

Для e : r ≃r s справедливо равенство r x (e.symm y) ↔ s (e x) y, выражающее совместимость симметрии с отображением RelIso.

LaTeX

$$$$ \forall {\alpha,\beta,\gamma,\delta} \ (e : r \equiv r s)\ {x:\alpha} {y:\beta},\ r(x, e.symm(y)) \leftrightarrow s(e(x), y). $$$$

Lean4

theorem symm_apply_rel (e : r ≃r s) {x y} : r (e.symm x) y ↔ s x (e y) := by rw [← e.map_rel_iff, e.apply_symm_apply]

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