congr_right — Mathlib

English

If h is a OneOneEquiv between q and r, then p ≤₁ q iff p ≤₁ r.

Русский

Если q и r эквивалентны по отношению OneOneEquiv, тогда p редуцируется к q эквивалентно p редуцируется к r.

LaTeX

$$$ p \\le_1 q \\iff p \\le_1 r $$$

Lean4

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

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