irreflexive — Mathlib

English

If r is irreflexive, then the inverse image relation via f is irreflexive.

Русский

Если r иррефлексивно, то обратная проекция через f иррефлексивна.

LaTeX

$$$\forall {\alpha \beta} (r : \beta \rightarrow \beta \rightarrow \mathrm{Prop}) (f : \alpha \rightarrow \beta), \ \mathrm{Irreflexive}(r) \rightarrow \mathrm{Irreflexive}(\mathrm{InvImage}(r,f))$$$

Lean4

theorem irreflexive (h : Irreflexive r) : Irreflexive (InvImage r f) := fun (a : α) (h₁ : InvImage r f a a) ↦ h (f a) h₁

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