head'_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem head'_iff : TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c :=
  by
  refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩
  induction h with
  | single hac => exact ⟨_, hac, by rfl⟩
  | tail _ hbc IH =>
    rcases IH with ⟨d, had, hdb⟩
    exact ⟨_, had, hdb.tail hbc⟩

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