English
If a < b in a linear order, there exist a' > a and b' < b such that for all x < a' and all y > b', x < y.
Русский
Если a < b в линейном порядке, то существуют a' > a и b' < b такие, что для всех x < a' и всех y > b' выполняется x < y.
LaTeX
$$exists a', b' with a' > a, b' < b and ∀ x < a', ∀ y > b', x < y$$
Lean4
/-- If `a < b` then there exist `a' > a` and `b' < b` such that `Set.Iio a'` is strictly to the left
of `Set.Ioi b'`. -/
theorem exists_disjoint_Iio_Ioi (h : a < b) : ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y :=
by
by_cases h' : a ⋖ b
· exact ⟨b, h, a, h, fun x hx y hy => hx.trans_le <| h'.ge_of_gt hy⟩
· rcases h.exists_lt_lt h' with ⟨c, ha, hb⟩
exact ⟨c, ha, c, hb, fun _ h₁ _ => lt_trans h₁⟩
