congr_left — Mathlib

English

If p is OneOneEquiv to q, then p ≤₁ r is equivalent to q ≤₁ r.

Русский

Если p эквивалентно q, то редуцируемость p к r эквивалентна редуцируемости q к r.

LaTeX

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

Lean4

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

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