le_one_iff

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.NeBot.le_one_iff

English

If f is NeBot, then f ≤ 1 iff f = 1.

Русский

Если f не ноль-верхний, тогда f ≤ 1 тогда и только тогда, когда f = 1.

LaTeX

$$$f.NeBot \\rightarrow (f \\le 1 \\iff f = 1)$$$

Lean4

@[to_additive]
protected theorem le_one_iff (h : f.NeBot) : f ≤ 1 ↔ f = 1 :=
  h.le_pure_iff

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

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

Разделы

Аффилиация

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