case h.e'_2
α : Type ?u.2316263
β : Type ?u.2316266
γ : Type ?u.2316269
γ₂ : Type ?u.2316272
δ : Type ?u.2316275
ι : Sort y
s t u : Set α
⊢ (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) = {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}
α : Type ?u.2316263
β : Type ?u.2316266
γ : Type ?u.2316269
γ₂ : Type ?u.2316272
δ : Type ?u.2316275
ι : Sort y
s t u : Set α
⊢ IsPiSystem (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b})
convert isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)
case h.e'_2.h
α : Type ?u.2316263
β : Type ?u.2316266
γ : Type ?u.2316269
γ₂ : Type ?u.2316272
δ : Type ?u.2316275
ι : Sort y
s t u : Set α
x : Set ℝ
⊢ (x ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) ↔ x ∈ {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}
case h.e'_2
α : Type ?u.2316263
β : Type ?u.2316266
γ : Type ?u.2316269
γ₂ : Type ?u.2316272
δ : Type ?u.2316275
ι : Sort y
s t u : Set α
⊢ (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) = {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}
ext x
no goals
case h.e'_2.h
α : Type ?u.2316263
β : Type ?u.2316266
γ : Type ?u.2316269
γ₂ : Type ?u.2316272
δ : Type ?u.2316275
ι : Sort y
s t u : Set α
x : Set ℝ
⊢ (x ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) ↔ x ∈ {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}
simp [eq_comm]