is_bot_of_is_min — Mathlib

English

If a directedOn set satisfies certain minimality, then for each a ∈ s, m ≤ a.

Русский

Если множество направлено и удовлетворяет условию минимальности, то для каждого a ∈ s выполняется m ≤ a.

LaTeX

$$$\forall a \in s,\ m \le a$ under hypotheses hd, hm, hmin$$$

Lean4

theorem is_bot_of_is_min {s : Set α} (hd : DirectedOn (· ≥ ·) s) {m} (hm : m ∈ s) (hmin : ∀ a ∈ s, a ≤ m → m ≤ a) :
    ∀ a ∈ s, m ≤ a := fun a as =>
  let ⟨x, xs, xm, xa⟩ := hd m hm a as
  (hmin x xs xm).trans xa

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