mono_on — Mathlib

English

If s is an antichain for r1 and the pairwise implication r2 a b → r1 a b holds for all pairs in s, then s is an antichain for r2.

Русский

Если s является антицепой по r1 и для всех пар a,b ∈ s выполняется r2 a b → r1 a b, то s — антицепь по r2.

LaTeX

$$$IsAntichain(r1,s) \\text{ and } s.Pairwise(\\lambda a b, r2 a b \to r1 a b) \\Rightarrow IsAntichain(r2,s)$$$

Lean4

theorem mono_on (hs : IsAntichain r₁ s) (h : s.Pairwise fun ⦃a b⦄ => r₂ a b → r₁ a b) : IsAntichain r₂ s :=
  hs.imp_on <| h.imp fun _ _ h h₁ h₂ => h₁ <| h h₂

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