rel_congr — Mathlib

English

Let r be a symmetric and transitive relation on α. For all a,b,c,d in α, if r(a,b) and r(c,d), then r(a,c) is equivalent to r(b,d).

Русский

Пусть r — симметричное и транзитивное отношение на α. Для любых a,b,c,d ∈ α верно: r(a,b) и r(c,d) ⇒ r(a,c) ⇔ r(b,d).

LaTeX

$$$\\\\forall a,b,c,d \\\\in \\\\alpha, \\\\ r a b \\\\to \\\\ r c d \\\\to \\\\ (r a c \\\\leftrightarrow \\\\ r b d).$$$

Lean4

theorem rel_congr [IsSymm α r] [IsTrans α r] {a b c d : α} (h₁ : r a b) (h₂ : r c d) : r a c ↔ r b d := by
  rw [rel_congr_left h₁, rel_congr_right h₂]

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