manyOneReducible_toNat_toNat — Mathlib

English

ManyOneReducible (toNat p) (toNat q) is equivalent to ManyOneReducible p q.

Русский

Редукция от toNat p к toNat q эквивалентна редукции p к q.

LaTeX

$$$ \\ManyOneReducible (toNat\\ p) (toNat\\ q) \\iff \\ManyOneReducible p q $$$

Lean4

@[simp]
theorem manyOneReducible_toNat_toNat {p : Set α} {q : Set β} : toNat p ≤₀ toNat q ↔ p ≤₀ q :=
  ⟨fun h => manyOneReducible_toNat.trans (h.trans toNat_manyOneReducible), fun h =>
    toNat_manyOneReducible.trans (h.trans manyOneReducible_toNat)⟩

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