no goals
α : Type u_1
β : Type ?u.41709
γ : Type ?u.41712
δ : Type ?u.41715
ι : Sort ?u.41718
κ : ι → Sort ?u.41723
inst✝ : Lattice α
s t : Interval α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t
classical
  rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
  rfl
α : Type u_1
β : Type ?u.41709
γ : Type ?u.41712
δ : Type ?u.41715
ι : Sort ?u.41718
κ : ι → Sort ?u.41723
inst✝ : Lattice α
s t : Interval α
⊢ ↑s ⊓ ↑t ≤ ⊥ ↔ ↑s ∩ ↑t ⊆ ↑⊥
α : Type u_1
β : Type ?u.41709
γ : Type ?u.41712
δ : Type ?u.41715
ι : Sort ?u.41718
κ : ι → Sort ?u.41723
inst✝ : Lattice α
s t : Interval α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t
rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
no goals
α : Type u_1
β : Type ?u.41709
γ : Type ?u.41712
δ : Type ?u.41715
ι : Sort ?u.41718
κ : ι → Sort ?u.41723
inst✝ : Lattice α
s t : Interval α
⊢ ↑s ⊓ ↑t ≤ ⊥ ↔ ↑s ∩ ↑t ⊆ ↑⊥
rfl