maximal_preimage_top — Mathlib

English

Let f: α → β be strictly monotone, α linear, β preorder with top. If f(a) = ⊤, then for every x ∈ α we have x ≤ a.

Русский

Пусть f: α → β строго монотонна; α линейный порядок, β — предорядок с верхней границей. Если f(a) = ⊤, то для каждого x ∈ α верно x ≤ a.

LaTeX

$$$\\text{If } f(a)=\\top, \\text{ then } \\forall x\\, (x \\le a).$$$

Lean4

theorem maximal_preimage_top [LinearOrder α] [Preorder β] [OrderTop β] {f : α → β} (H : StrictMono f) {a}
    (h_top : f a = ⊤) (x : α) : x ≤ a :=
  H.maximal_of_maximal_image
    (fun p => by
      rw [h_top]
      exact le_top)
    x

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