antitoneOn_univ

Mathlib.Order.Monotone.Defs

URI: https://scilib.ai/kg/mathlib#antitoneOn_univ

English

AntitoneOn on the universal set is equivalent to Antitone.

Русский

Антитонность на всём множестве эквивалентна антитонности функции.

LaTeX

$$$\operatorname{AntitoneOn}(f,\mathrm{Set.univ}) \leftrightarrow \operatorname{Antitone}(f)$$$

Lean4

@[simp]
theorem antitoneOn_univ : AntitoneOn f Set.univ ↔ Antitone f :=
  ⟨fun h _ _ ↦ h trivial trivial, fun h ↦ h.antitoneOn _⟩

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

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

Разделы

Аффилиация

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