bounded_gt_Ici — Mathlib

English

For every a, the set { x ∈ α | x ≥ a } is bounded above with respect to >; equivalently, there exists a bound c with ∀ x ≥ a, x > c.

Русский

Для каждого a множество { x ∈ α | x ≥ a } ограничено сверху по отношению >, то есть существует C, такая что для всех x ≥ a, x > C.

LaTeX

$$$\forall a:\ Bound\ ed\ (>)(Ici\ a)$$$

Lean4

theorem bounded_gt_Ici [Preorder α] [NoMinOrder α] (a : α) : Bounded (· > ·) (Ici a) := by
  simp only [← bounded_ge_iff_bounded_gt, bounded_ge_Ici]

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