disjoin_left

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#OneOneReducible.disjoin_left

← MathLib Explorer

English

p is reducible to the left embedding of p into p ⊕' q.

Русский

p редуцируется к левой части суммирования p ⊕' q.

LaTeX

$$$ p \\le_1 p \\oplus' q $$$

Lean4

theorem disjoin_left {α β} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} : p ≤₁ p ⊕' q :=
  ⟨Sum.inl, Computable.sumInl, fun _ _ => Sum.inl.inj_iff.1, fun _ => Iff.rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru