mono — Mathlib

English

If f ~_l' g and l ≤ l', then f ~_l g; i.e., weaker limits preserve equivalence when the filter becomes coarser.

Русский

Если f эквивалентно g по l' и l ≤ l', то по более грубому фильтру l также сохраняется эквивалентность.

LaTeX

$$f ~[l'] g \Rightarrow l \le l' \Rightarrow f ~[l] g$$

Lean4

theorem mono {f g : α → β} {l' : Filter α} (h : f ~[l'] g) (hl : l ≤ l') : f ~[l] g :=
  IsLittleO.mono h hl

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