map_rel_iff — Mathlib

English

If f is a relation isomorphism between r and s, then for any a,b, s(f(a), f(b)) holds iff r(a,b) holds.

Русский

Если f является отображением-реляционным изоморфизмом между r и s, то для любых a,b верно: s(f(a), f(b)) тогда и только тогда, когда r(a,b).

LaTeX

$$$(f : r \simeq_r s) {a b} \colon s(f(a),f(b)) \iff r(a,b)$$$

Lean4

theorem map_rel_iff (f : r ≃r s) {a b} : s (f a) (f b) ↔ r a b :=
  f.map_rel_iff'

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