absorbing — Mathlib

English

The filter absorbing u is the Filter on α consisting of all sets s with Absorbs G0 s u, i.e., a filter defined by absorption relative to u.

Русский

Фильтр, который поглощает u, состоит из всех множеств s с Absorbs G0 s u; это определение фильтра через поглощение относительно u.

LaTeX

$$$\text{absorbing}(G_0)\,u = \{s \subseteq \alpha \mid Absorbs\ G_0\ s\ u\}$$$

Lean4

/-- The filter of sets that absorb `u`. -/
def absorbing : Filter α where
  sets := {s | Absorbs G₀ s u}
  univ_sets := .univ
  sets_of_superset h := h.mono_left
  inter_sets := .inter

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