English
If t1 is bounded by o1 up to x and t2 is bounded from x to o2, then every element of t1 is less than every element of t2.
Русский
Если t1 ограничено справа x и слева o1, а t2 ограничено слева x и справа o2, то каждый элемент t1 меньше любого элемента t2.
LaTeX
$$$\forall t_1\ t_2\ o_1\ o_2\ x: (Bounded\ t_1\ o_1\ (x:WithTop\ α)) \, (Bounded\ t_2\ (x:WithBot\ α)\ o_2) \Rightarrow (t_1.All(\lambda y. t_2.All(\lambda z. y < z)))$$$
Lean4
theorem to_sep {t₁ t₂ o₁ o₂} {x : α} (h₁ : Bounded t₁ o₁ (x : WithTop α)) (h₂ : Bounded t₂ (x : WithBot α) o₂) :
t₁.All fun y => t₂.All fun z : α => y < z :=
by
refine h₁.mem_lt.imp fun y yx => ?_
exact h₂.mem_gt.imp fun z xz => lt_trans yx xz
