isIrrefl — Mathlib

English

If a relation-homomorphism f : F from r to s exists and s is irreflexive, then r is irreflexive.

Русский

Если существует отображение, сохраняющее отношение, и отношение s иррефлексивно, то и r иррефлексиво.

LaTeX

$$$\forall f,\ [\text{RelHomClass } F\ r\ s]\ \bigl([\operatorname{IsIrrefl}\ \beta\ s]\Rightarrow \operatorname{IsIrrefl}\ \alpha\ r\bigr)$$$

Lean4

protected theorem isIrrefl [RelHomClass F r s] (f : F) : ∀ [IsIrrefl β s], IsIrrefl α r
  | ⟨H⟩ => ⟨fun _ h => H _ (map_rel f h)⟩

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