bounded_ge_inter_not_ge — Mathlib

English

For any SemilatticeInf α and a ∈ α, Bounded(≥) on s ∩ {b | ¬ a ≤ b} is equivalent to Bounded(≥) on s.

Русский

Для семилатерал-инфа α и элемента a: ограниченность по ≥ на множество s ∩ {b | ¬ a ≤ b} эквивалентна ограниченности по ≥ на s.

LaTeX

$$$ \operatorname{Bounded}(\ge)\left(s \cap \{ b \mid \neg a \le b\} \right) \iff \operatorname{Bounded}(\ge) s $$$

Lean4

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

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