congr_antitoneOn — Mathlib

English

If f1 and f2 agree on s, then AntitoneOn f1 s is equivalent to AntitoneOn f2 s.

Русский

Если f1 и f2 совпадают на s, то AntitoneOn(f1,s) эквивалентно AntitoneOn(f2,s).

LaTeX

$$$\\forall {\\alpha}, {\\beta}, {\\gamma},\\ s: Set\\alpha,\\ f_1,f_2: \\alpha \\to \\beta,\\ [Preorder\\alpha][Preorder\\beta]\\n( h : s.EqOn f_1 f_2 s ) \\to \\operatorname{AntitoneOn} f_1 s \\iff \\operatorname{AntitoneOn} f_2 s$$$

Lean4

theorem congr_antitoneOn (h : s.EqOn f₁ f₂) : AntitoneOn f₁ s ↔ AntitoneOn f₂ s :=
  ⟨fun h₁ => h₁.congr h, fun h₂ => h₂.congr h.symm⟩

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