le_def — Mathlib

English

For filters f,g on α, the order relation satisfies f ≤ g iff ∀ x ∈ g, x ∈ f, i.e., every set in g is also in f.

Русский

Для фильтров f и g на α выполняется, что f ≤ g тогда и только тогда, когда для любого множества x, принадлежащее g, x принадлежит f.

LaTeX

$$$f \\le g \\iff \\forall x : Set \\alpha, x \\in g \\to x \\in f$$$

Lean4

theorem le_def : f ≤ g ↔ ∀ x ∈ g, x ∈ f :=
  Iff.rfl

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