English
In a linear order γ, for each i ∈ γ there exists j that is the least upper bound of the set Iio(i) = { x ∈ γ | x < i }.
Русский
В линейном порядке γ для каждого i ∈ γ существует наименьшая верхняя граница множества Iio(i) = { x ∈ γ | x < i }.
LaTeX
$$$ \forall i \in \gamma, \ exists\ j,\ IsLUB(Iio(i))\ j. $$$
Lean4
theorem exists_lub_Iio (i : γ) : ∃ j, IsLUB (Iio i) j :=
by
by_cases h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
· obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩
· refine ⟨i, fun j hj => le_of_lt hj, ?_⟩
rw [mem_lowerBounds]
by_contra h
refine h_exists_lt ?_
push_neg at h
exact h
