instSup — Mathlib

English

The supremum of two filters is the filter that contains sets that belong to both filters; equivalently, the supremum is their intersection.

Русский

Супремум двух фильтров — это фильтр, содержащий множества, принадлежащие обоим фильтрам; эквивалентно это их пересечение.

LaTeX

$$$f \\lor g = f \\cap g$$$

Lean4

/-- The supremum of two filters is the filter that contains sets that belong to both filters. -/
instance instSup : Max (Filter α) where max f g := .copy (sSup { f, g }) {s | s ∈ f ∧ s ∈ g} <| by simp

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