α : Type u_1
β : Type ?u.186303
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a₁ ∩ Iic b₁ ∩ (Ioi a₂ ∩ Iic b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iic b₁ ∩ Iic b₂)
α : Type u_1
β : Type ?u.186303
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
simp only [Ioi_inter_Iic.symm, Ioi_inter_Ioi.symm, Iic_inter_Iic.symm]
no goals
α : Type u_1
β : Type ?u.186303
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi a₁ ∩ Iic b₁ ∩ (Ioi a₂ ∩ Iic b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iic b₁ ∩ Iic b₂)
ac_rfl