map_lt_map — Mathlib

English

Monotonicity of map: mapping preserves order.

Русский

Монотонность отображения: отображение сохраняет порядок.

LaTeX

$$$$ \\forall f:\\alpha\\to\\beta, \\ \\operatorname{Monotone}(\\operatorname{map} f) $$$$

Lean4

@[simp, gcongr]
theorem map_lt_map {f : α → β} {s t : Multiset α} (h : s < t) : s.map f < t.map f :=
  by
  refine (map_le_map h.le).lt_of_not_ge fun H => h.ne <| eq_of_le_of_card_le h.le ?_
  rw [← s.card_map f, ← t.card_map f]
  exact card_le_card H

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