monotone_smallSets — Mathlib

English

The operator smallSets is monotone on filters: if l ≤ l' then l.smallSets ≤ l'.smallSets.

Русский

Оператор smallSets монотонен по отношению к фильтрам: если l ≤ l', то l.smallSets ≤ l'.smallSets.

LaTeX

$$$\forall l\, l' : \text{Filter}(\alpha),\; l \le l' \Rightarrow l.smallSets \le l'.smallSets$$$

Lean4

@[mono]
theorem monotone_smallSets : Monotone (@smallSets α) :=
  monotone_lift' monotone_id monotone_const

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