antivary_id_iff

Mathlib.Order.Monotone.Monovary

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

English

Antivary f id is equivalent to Antitone f.

Русский

Antivary f id эквивалентно Antitone f.

LaTeX

$$$\operatorname{Antivary}(f,\mathrm{id}) \iff \operatorname{Antitone}(f)$$$

Lean4

@[simp]
theorem antivary_id_iff : Antivary f id ↔ Antitone f :=
  antitone_iff_forall_lt.symm

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

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

Разделы

Аффилиация

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