coe_pos

Mathlib.Order.Filter.FilterProduct

URI: https://scilib.ai/kg/mathlib#Filter.Germ.coe_pos

English

For a Preorder β with a Zero, 0 < f* iff eventually 0 < f(x).

Русский

Для предпорядка β с нулём: 0 < f* тогда и только тогда, когда в конечном большинстве x выполняется 0 < f(x).

LaTeX

$$$0 < (f : β^*) \\iff \\forall^* x, 0 < f(x).$$$

Lean4

theorem coe_pos [Preorder β] [Zero β] {f : α → β} : 0 < (f : β*) ↔ ∀* x, 0 < f x :=
  coe_lt

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

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

Разделы

Аффилиация

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