mem_inv — Mathlib

English

For any α, β and a relation R between α and β, the inverse relation relates b to a if and only if a relates to b by R; i.e., b ~[R.inv] a ⇔ a ~[R] b.

Русский

Для любых множест α, β и отношения R между ними верно, что b относится к a по обратному отношению, если и только если a относится к b по R: b ~[R.inv] a ⇔ a ~[R] b.

LaTeX

$$$b \sim_{R^{-1}} a \iff a \sim_{R} b$$$

Lean4

@[simp]
theorem mem_inv : b ~[R.inv] a ↔ a ~[R] b :=
  .rfl

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