transGen_reflGen — Mathlib

English

The transitive closure of the reflexive generator equals the reflexive-transitive closure.

Русский

Транзитивное замыкание рефлексивного генератора равно рефлексивно-транзитивному замыканию.

LaTeX

$$$$\\operatorname{TransGen}(\\operatorname{ReflGen} r) = \\operatorname{ReflTransGen} r$$$$

Lean4

@[simp]
theorem transGen_reflGen : TransGen (ReflGen r) = ReflTransGen r :=
  by
  ext x y
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simpa [reflTransGen_idem] using TransGen.to_reflTransGen <| TransGen.mono (fun _ _ ↦ ReflGen.to_reflTransGen) h
  · obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
    · exact .single .refl
    · exact TransGen.mono (fun _ _ ↦ .single) h

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