unbounded_gt_inter_not_gt — Mathlib

English

In a SemilatticeInf setting, no lower bound for s ∩ {b | not (a < b)} with respect to > is equivalent to no lower bound for s with respect to >.

Русский

В рамках полуправильного частичного порядка без нижней границы по > для пересечения s с {b | не (a < b)} эквивалентно отсутствию нижней границы по > для s.

LaTeX

$$$\forall m\, \exists x\in s\cap\{y\;|\; \neg(am \;\Longleftrightarrow\; \forall m\, \exists x\in s,\; x>m$$$

Lean4

theorem unbounded_gt_inter_not_gt [SemilatticeInf α] (a : α) :
    Unbounded (· > ·) (s ∩ {b | ¬a < b}) ↔ Unbounded (· > ·) s :=
  @unbounded_lt_inter_not_lt αᵒᵈ s _ a

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