monotone_map — Mathlib

English

The map operator by any fixed functor F is monotone: if P ≤ Q then P.map F ≤ Q.map F.

Русский

Оперирование map на фиксированном функторе F сохраняет упорядочение; если P ≤ Q, то P.map F ≤ Q.map F.

LaTeX

$$$\\text{Monotone}(\\mathrm{map}\\;\\cdot\\;F).$$$

Lean4

theorem monotone_map (F : C ⥤ D) : Monotone (map · F) :=
  by
  intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

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