cases_tail — Mathlib

English

A reflexive-transitive relation from a to b is either a=b or there exists a, with a relation from a to a and a relation to b by r in the tail.

Русский

Замыкание ReflTransGen r от a к b либо означает, что a = b, либо существует c such that a связаны с c через ReflTransGen r и r c b держит.

LaTeX

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

Lean4

theorem cases_tail : ReflTransGen r a b → b = a ∨ ∃ c, ReflTransGen r a c ∧ r c b :=
  (cases_tail_iff r a b).1

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