congr_left — Mathlib

English

If p ≃ q, then for any r a p ≃ r is equivalent to a q ≃ r.

Русский

Если p эквивалентно q, то для любого r верно: p ≃ r ⇔ q ≃ r.

LaTeX

$$$ (p \\sim q) \\Rightarrow (p \\sim r) \\iff (q \\sim r) $$$

Lean4

theorem congr_left {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop}
    (h : ManyOneEquiv p q) : ManyOneEquiv p r ↔ ManyOneEquiv q r :=
  and_congr h.le_congr_left h.le_congr_right

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