strictAnti_of_inj_boundedOrder — Mathlib

English

If a continuous injective function f on a bounded order is aligned such that f(top) ≤ f(bottom), then f is strictly antitone.

Русский

Если непрерывная инъективная функция на ограниченном порядке удовлетворяет условию, что верхняя граница не выше нижней, то функция строго антимонотонна.

LaTeX

$$StrictAnti f$$

Lean4

theorem strictAnti_of_inj_boundedOrder [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf : f ⊤ ≤ f ⊥)
    (hf_i : Injective f) : StrictAnti f :=
  hf_c.strictMono_of_inj_boundedOrder (δ := δᵒᵈ) hf hf_i

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