tail'_iff — Mathlib

English

TransGen r a c is equivalent to the existence of a b with a ReflTransGen r a b and r b c.

Русский

TransGen r a c эквивалентно существованию b, такого что ReflTransGen r a b и r b c.

LaTeX

$$$ TransGen r a c \leftrightarrow \exists b, ReflTransGen r a b \land r b c $$$

Lean4

theorem tail'_iff : TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c :=
  by
  refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩
  cases h with
  | single hac => exact ⟨_, by rfl, hac⟩
  | tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩

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