exists_glb_Ioi — Mathlib

English

For any i ∈ γ in a linear order, there exists j such that j is the greatest lower bound of the set Ioi(i) = { x ∈ γ | x > i }.

Русский

Для любого i ∈ γ в линейном порядке существует j такое, что j является наибольшей нижней границей множества Ioi(i) = { x > i }.

LaTeX

$$$ \exists j,\ IsGLB(Ioi(i))\ j. $$$

Lean4

theorem exists_glb_Ioi (i : γ) : ∃ j, IsGLB (Ioi i) j :=
  @exists_lub_Iio γᵒᵈ _ i

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