le_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 le_congr_right {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop}
    {r : γ → Prop} (h : OneOneEquiv q r) : p ≤₁ q ↔ p ≤₁ r :=
  ⟨fun h' => h'.trans h.1, fun h' => h'.trans h.2⟩

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