unbounded_ge_inter_not_ge — Mathlib

English

In an order dual of a semilatticeInf, Unbounded (≥) on s ∩ { b | ¬ a ≤ b } is equivalent to Unbounded (≥) on s.

Русский

В порядке-двойнике полусложения Inf, неограниченность ≥ на s ∩ { b | ¬ a ≤ b } эквивалентна неограниченности ≥ на s.

LaTeX

$$$$\mathrm{Unbounded}_{\ge}\left(s \cap \{b \mid \neg a \le b\}\right) \iff \mathrm{Unbounded}_{\ge}(s).$$$$

Lean4

theorem unbounded_ge_inter_not_ge [SemilatticeInf α] (a : α) :
    Unbounded (· ≥ ·) (s ∩ {b | ¬a ≤ b}) ↔ Unbounded (· ≥ ·) s :=
  @unbounded_le_inter_not_le αᵒᵈ s _ a

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