to_many_one — Mathlib

English

If p reduces to q in the one-to-one sense, then p reduces to q in the many-to-one sense.

Русский

Если p редуцируется к q в однозначной форме, то p редуцируется к q в форме многие–к–одному.

LaTeX

$$$\forall \alpha\beta\,\forall p:\alpha\to\mathrm{Prop}\,\forall q:\beta\to\mathrm{Prop},\ p\le_1 q\Rightarrow p\le_0 q$$$

Lean4

theorem to_many_one {α β} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} : p ≤₁ q → p ≤₀ q
  | ⟨f, c, _, h⟩ => ⟨f, c, h⟩

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