covariant_swap_div — Mathlib

English

The swapped division operator swap(· / ·) is monotone in its second argument. That is, for all f,g,g' ∈ Filter α and for all f ∈ Filter α, if g ≤ g' then g / f ≤ g' / f.

Русский

Обменное деление swap(· / ·) монотонно по второму аргументу: для любых f, g, g' в Filter(α) и если g ≤ g', то g / f ≤ g' / f.

LaTeX

$$$\forall f,g,g' \in \mathrm{Filter}(\alpha),\ g \le g' \Rightarrow g / f \le g' / f.$$$

Lean4

@[to_additive]
instance covariant_swap_div : CovariantClass (Filter α) (Filter α) (swap (· / ·)) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_right⟩

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