cases_head — Mathlib

English

Every ReflTransGen r a b is either a=b or there exists c with a r c and ReflTransGen r c b.

Русский

Каждое ReflTransGen r a b либо имеет вид a = b, либо существует c such that a r c и ReflTransGen r c b.

LaTeX

$$$ ∀ {α} {r} {a b : α}, \mathrm{ReflTransGen} r a b \to (a = b \lor ∃ c, r a c ∧ \mathrm{ReflTransGen} r c b) $$$

Lean4

theorem cases_head (h : ReflTransGen r a b) : a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b := by
  induction h using Relation.ReflTransGen.head_induction_on <;> grind

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