antitoneOn_singleton

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.antitoneOn_singleton

English

Antitone on singleton: if the domain is {a}, then f is antitone on {a}.

Русский

Антитонность на одиночном множестве: если область определения — {a}, то f антинотона на {a}.

LaTeX

$$$ \text{AntitoneOn}(f, \{ a \})$$$

Lean4

@[simp]
theorem antitoneOn_singleton : AntitoneOn f { a } :=
  subsingleton_singleton.antitoneOn f

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

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

Разделы

Аффилиация

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