lift' — Mathlib

English

If p respects r via f for all a,b, and hab is a ReflTransGen r path, then P (f a) (f b).

Русский

Если p сохраняет r через f для всех a,b и hab — путь ReflTransGen r, то ReflTransGen p (f a) (f b).

LaTeX

$$$$\\forall {a b} (f : \\alpha \\to \\beta) (h : \\forall a b, r a b \\to \\operatorname{ReflTransGen} p (f a) (f b)) (hab : \\operatorname{ReflTransGen} r a b) : \\operatorname{ReflTransGen} p (f a) (f b)$$$$

Lean4

theorem lift' {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → ReflTransGen p (f a) (f b))
    (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b) := by simpa [reflTransGen_idem] using hab.lift f h

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