le_congr_right — Mathlib

English

If q and r are ManyOneEquiv, then for any predicate p the statement “p reduces to q” is equivalent to “p reduces to r.”

Русский

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

LaTeX

$$$ p \\le_0 q \\iff p \\le_0 r $$$

Lean4

theorem le_congr_right {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop}
    {r : γ → Prop} (h : ManyOneEquiv q r) : p ≤₀ q ↔ p ≤₀ r :=
  ⟨fun h' => h'.trans h.1, fun h' => h'.trans h.2⟩

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