pith. machine review for the scientific record. sign in
theorem proved term proof

eq_of_reflTransGen

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  35theorem eq_of_reflTransGen {R : V → V → Prop} {f : V → ℝ}
  36    (hadj : ∀ a b, R a b → f a = f b) {u v : V}
  37    (huv : Relation.ReflTransGen R u v) : f u = f v := by

proof body

Term-mode proof.

  38  induction huv with
  39  | refl => rfl
  40  | tail _ hbc ih => exact ih.trans (hadj _ _ hbc)
  41
  42/-- On a preconnected graph (every pair related by ReflTransGen),
  43    agreement on edges implies global constancy. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.