reflTransGen_of_equivalence — Mathlib

English

If r is an equivalence and r' is contained in r, then a ReflTransGen step implies r a b.

Русский

Если r — эквивалентность и r' ⊆ r, то ReflTransGen r' от a к b implies r a b.

LaTeX

$$$$(\\\\forall a b, r' a b \\\\Rightarrow r a b) \\\\Rightarrow \\\\operatorname{ReflTransGen} r' a b \\\\Rightarrow r a b$$$$

Lean4

theorem reflTransGen_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) :
    (∀ a b, r' a b → r a b) → ReflTransGen r' a b → r a b :=
  reflTransGen_of_transitive_reflexive hr.1 (fun _ _ _ ↦ hr.trans)

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