reaches_total — Mathlib

English

If a reaches b and a reaches c, then either b reaches c or c reaches b.

Русский

Если a достигает b и a достигает c, то либо b достигает c, либо c достигает b.

LaTeX

$$$\\forall a\\,b\\,c\\; (\\mathrm{Reaches}\\ f\\ a\\ b) \\land (\\mathrm{Reaches}\\ f\\ a\\ c) \\Rightarrow (\\mathrm{Reaches}\\ f\\ b\\ c) \\lor (\\mathrm{Reaches}\\ f\\ c\\ b)$$$

Lean4

theorem reaches_total {σ} {f : σ → Option σ} {a b c} (hab : Reaches f a b) (hac : Reaches f a c) :
    Reaches f b c ∨ Reaches f c b :=
  ReflTransGen.total_of_right_unique (fun _ _ _ ↦ Option.mem_unique) hab hac

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