image — Mathlib

English

If a ≼ b, then for any monotone f, f a ≼ f b in the target order.

Русский

Если a ≼ b, тогда для любого монотонного отображения f, f a ≼ f b в целевом порядке.

LaTeX

$$$\\forall a,b \\in α,\\ AntisymmRel(≤) a b \\to ∀ f,\\ Monotone f \\to AntisymmRel(≤) (f a) (f b)$$$

Lean4

theorem image (h : AntisymmRel (· ≤ ·) a b) {f : α → β} (hf : Monotone f) : AntisymmRel (· ≤ ·) (f a) (f b) :=
  ⟨hf h.1, hf h.2⟩

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