reflTransGen_iff_eq_or_transGen — Mathlib

English

Every ReflTransGen r a b path is either trivial with a = b or contains a nontrivial TransGen path from a to b.

Русский

Каждый путь ReflTransGen r a b либо тривиален (a = b), либо содержит непустой путь TransGen r a b от a до b.

LaTeX

$$$$\\operatorname{ReflTransGen} r a b \\iff a = b \\lor \\operatorname{TransGen} r a b$$$$

Lean4

theorem reflTransGen_iff_eq_or_transGen : ReflTransGen r a b ↔ b = a ∨ TransGen r a b :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  ·
    cases h with
    | refl => exact Or.inl rfl
    | tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)
  · rcases h with (rfl | h)
    · rfl
    · exact h.to_reflTransGen

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