is_top_of_is_max — Mathlib

English

If s is directed under ≤, and m ∈ s, and m ≤ a → a ≤ m for all a ∈ s, then a ≤ m for all a ∈ s.

Русский

Если s направлено по ≤, m ∈ s и ∀ a ∈ s, m ≤ a → a ≤ m, то ∀ a ∈ s, a ≤ m.

LaTeX

$$$\text{DirectedOn}(\le, s) \rightarrow \forall m\in s, (\forall a\in s, m \le a \rightarrow a \le m) \rightarrow \forall a\in s, a \le m$$$

Lean4

theorem is_top_of_is_max {s : Set α} (hd : DirectedOn (· ≤ ·) s) {m} (hm : m ∈ s) (hmax : ∀ a ∈ s, m ≤ a → a ≤ m) :
    ∀ a ∈ s, a ≤ m :=
  @DirectedOn.is_bot_of_is_min αᵒᵈ _ s hd m hm hmax

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