reflTransGen_of_transitive_reflexive

English

If r is reflexive and transitive, and r' is contained in r, and there is a ReflTransGen path from a to b via r', then r relates a to b.

Русский

Пусть r рефлексивно и транзитивно, и r' ⊆ r. Если существует путь ReflTransGen от a к b через r', то выполняется r a b.

LaTeX

$$$\\\\operatorname{ReflTransGen} r' a b \\\\Rightarrow r a b$$$

Lean4

theorem reflTransGen_of_transitive_reflexive {r' : α → α → Prop} (hr : Reflexive r) (ht : Transitive r)
    (h : ∀ a b, r' a b → r a b) (h' : ReflTransGen r' a b) : r a b := by
  induction h' with
  | refl => exact hr _
  | tail _ hbc ih => exact ht ih (h _ _ hbc)

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