isLUB_lowerBounds — Mathlib

English

There is an equivalence: IsLUB(lowerBounds(s), a) if and only if IsGLB(s, a).

Русский

Существуют эквивалентности: IsLUB(нижние границы s, a) эквивалентно IsGLB(s, a).

LaTeX

$$$IsLUB(\operatorname{lowerBounds}(s), a) \leftrightarrow IsGLB(s, a)$$$

Lean4

@[simp]
theorem isLUB_lowerBounds : IsLUB (lowerBounds s) a ↔ IsGLB s a :=
  ⟨fun H => ⟨fun _ hx => H.2 <| subset_upperBounds_lowerBounds s hx, H.1⟩, IsGreatest.isLUB⟩

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