strictAntiOn

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.strictAntiOn

English

If s is a subsingleton, then f is strictly antitone on s: for a,b ∈ s, a < b implies f(a) > f(b).

Русский

Если s — пододиноство, то f строго антитонна на s: для a,b ∈ s, если a < b, то f(a) > f(b).

LaTeX

$$$ \forall x,y \in s, x < y \Rightarrow f(x) > f(y)$$$

Lean4

protected theorem strictAntiOn (h : s.Subsingleton) : StrictAntiOn f s := fun _ ha _ hb hlt => (hlt.ne (h ha hb)).elim

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru