comap_mono — Mathlib

English

If s ≤ t are opens in β, then comap f s ≤ comap f t in α.

Русский

Если s ≤ t в β, то их обратные изображения через f удовлетворяют тому же неравенству в α.

LaTeX

$$$f : C(\alpha,\beta)\;\{s,t : Opens(\beta)\} \ (s \le t) \Rightarrow comap f s \le comap f t$$$

Lean4

theorem comap_mono (f : C(α, β)) {s t : Opens β} (h : s ≤ t) : comap f s ≤ comap f t :=
  OrderHomClass.mono (comap f) h

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