reflTransGen_iff_eq — Mathlib

English

If r has no successor from a, then the reflexive-transitive closure from a to b holds exactly when b = a.

Русский

Если из вершины a нельзя перейти по r к чему-либо другому, то ReflTransGen r a b истинно тогда и только тогда, когда b = a.

LaTeX

$$$$\\forall {α} {r : α \\to α \\to \\mathrm{Prop}} (h : \\forall b, \\neg r a b) : \\operatorname{ReflTransGen} r a b \\iff b = a$$$$

Lean4

theorem reflTransGen_iff_eq (h : ∀ b, ¬r a b) : ReflTransGen r a b ↔ b = a := by rw [cases_head_iff]; simp [h, eq_comm]

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