ι : Type ?u.205943
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a < c → b < c → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)
ι : Type ?u.205943
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a < c → b < c → ¬c ∈ [[a, b]]
rw [mem_uIcc]
no goals
ι : Type ?u.205943
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a < c → b < c → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)
exact Set.not_mem_uIcc_of_gt