isChain_range — Mathlib

English

A more explicit form: if ∀x,y, r x y → s(f x) (f y), and c is a chain under r, then f''c is a chain under s.

Русский

Более явная форма: если ∀x,y, r x y → s(f x) (f y), и c — цепь под r, то образ f[c] — цепь под s.

LaTeX

$$$\operatorname{IsChain}(r,c) \to (\forall x,y, r x y \to s (f x) (f y)) \to \operatorname{IsChain}(s, \mathrm{image}_f(c))$$$

Lean4

theorem isChain_range [LinearOrder α] [Preorder β] {f : α → β} (hf : Monotone f) : IsChain (· ≤ ·) (range f) :=
  by
  rw [← image_univ]
  exact hf.isChain_image (isChain_of_trichotomous _)

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