minimal_preimage_bot — Mathlib

English

Let f: α → β be strictly monotone with β having a bottom element ⊥. If f a = ⊥, then for all x ∈ α we have a ≤ x.

Русский

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

LaTeX

$$$f(a) = \\bot \\implies a \\le x$ для всех x ∈ α; более precisely: $f(a) = \\bot \\,\\Rightarrow \\, a \\le x$.$$

Lean4

theorem minimal_preimage_bot [LinearOrder α] [Preorder β] [OrderBot β] {f : α → β} (H : StrictMono f) {a}
    (h_bot : f a = ⊥) (x : α) : a ≤ x :=
  H.minimal_of_minimal_image
    (fun p => by
      rw [h_bot]
      exact bot_le)
    x

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