ι : Type u_1
M : Type ?u.20595
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})
ι : Type u_1
M : Type ?u.20595
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (splitLower I i x) (splitUpper I i x)
rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]
ι : Type u_1
M : Type ?u.20595
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint {y | y i ≤ x} {y | x < y i}
ι : Type u_1
M : Type ?u.20595
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})
refine' (Disjoint.inf_left' _ _).inf_right' _
ι : Type u_1
M : Type ?u.20595
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → ¬a ∈ {y | x < y i}
ι : Type u_1
M : Type ?u.20595
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint {y | y i ≤ x} {y | x < y i}
rw [Set.disjoint_left]
no goals
ι : Type u_1
M : Type ?u.20595
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → ¬a ∈ {y | x < y i}
exact fun y (hle : y i ≤ x) hlt => not_lt_of_le hle hlt