congr_strictAntiOn — Mathlib

English

Let s be a subset of α and f1, f2: α → β. If f1 and f2 agree on s (i.e., f1(x) = f2(x) for all x ∈ s), then f1 is strictly antitone on s if and only if f2 is strictly antitone on s.

Русский

Пусть s ⊆ α и f1, f2: α → β. Если f1 и f2 совпадают на s (f1(x) = f2(x) для всех x ∈ s), то f1 строго антитонична на s тогда и только тогда, когда f2 строго антитонична на s.

LaTeX

$$$\big(\forall x \in s,\ f_1(x)=f_2(x)\big) \Rightarrow \big(\operatorname{StrictAntiOn}(f_1,s) \iff \operatorname{StrictAntiOn}(f_2,s)\big)$$$

Lean4

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

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