elim

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.MemUnion.elim

English

From x ∈ a ∪ b, with proofs that x ∈ a → P and x ∈ b → P, deduce P.

Русский

Из x ∈ a ∪ b и доказательств x ∈ a → P, x ∈ b → P следует P.

LaTeX

$$$(x \in a \cup b) \rightarrow (x \in a \rightarrow P) \rightarrow (x \in b \rightarrow P) \rightarrow P$$$

Lean4

theorem elim {x : α} {a b : Set α} {P : Prop} (H₁ : x ∈ a ∪ b) (H₂ : x ∈ a → P) (H₃ : x ∈ b → P) : P :=
  Or.elim H₁ H₂ H₃

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

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

Разделы

Аффилиация

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