Theorem: UpperLowerContinuous.lower_basis (Compfiles/UpperLowerContinuous.lean)

State before:
⊢ TopologicalSpace.IsTopologicalBasis lower_intervals
Tactic:
refine
 @TopologicalSpace.IsTopologicalBasis.mk ℝ tₗ lower_intervals ?_ ?_ rfl
State after:
case refine_1

⊢ ∀ t₁ ∈ lower_intervals, ∀ t₂ ∈ lower_intervals, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

case refine_2

⊢ ⋃₀ lower_intervals = Set.univ

State before:
case refine_1

⊢ ∀ t₁ ∈ lower_intervals, ∀ t₂ ∈ lower_intervals, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
Tactic:
intro I1 hI1 I2 hI2 x hx
State after:
case refine_1
I1 : Set ℝ
hI1 : I1 ∈ lower_intervals
I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2

State before:
case refine_1
I1 : Set ℝ
hI1 : I1 ∈ lower_intervals
I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
obtain ⟨a, b, hab⟩ := hI1
State after:
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2

State before:
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ lower_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
obtain ⟨c, d, hcd⟩ := hI2
State after:
case refine_1.intro.intro.intro.intro
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2

State before:
case refine_1.intro.intro.intro.intro
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
Tactic:
use Set.Ico (Sup.sup a c) (Inf.inf b d)
State after:
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals ∧ x ∈ Set.Ico (a ⊔ c) (b ⊓ d) ∧ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2

State before:
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals ∧ x ∈ Set.Ico (a ⊔ c) (b ⊓ d) ∧ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
constructor
State after:
case h.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals

case h.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ x ∈ Set.Ico (a ⊔ c) (b ⊓ d) ∧ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2

State before:
case h.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ∈ lower_intervals
Tactic:
exact ⟨Sup.sup a c, Inf.inf b d, rfl ⟩
State after:
no goals

State before:
case h.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ x ∈ Set.Ico (a ⊔ c) (b ⊓ d) ∧ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
constructor
State after:
case h.right.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ x ∈ Set.Ico (a ⊔ c) (b ⊓ d)

case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2

State before:
case h.right.left
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ x ∈ Set.Ico (a ⊔ c) (b ⊓ d)
Tactic:
aesop
State after:
no goals

State before:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
⊢ Set.Ico (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2
Tactic:
intro y hy
State after:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
y : ℝ
hy : y ∈ Set.Ico (a ⊔ c) (b ⊓ d)
⊢ y ∈ I1 ∩ I2

State before:
case h.right.right
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ico a b = I1
c d : ℝ
hcd : Set.Ico c d = I2
y : ℝ
hy : y ∈ Set.Ico (a ⊔ c) (b ⊓ d)
⊢ y ∈ I1 ∩ I2
Tactic:
aesop
State after:
no goals

State before:
case refine_2

⊢ ⋃₀ lower_intervals = Set.univ
Tactic:
ext x
State after:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ lower_intervals ↔ x ∈ Set.univ

State before:
case refine_2.h
x : ℝ
⊢ x ∈ ⋃₀ lower_intervals ↔ x ∈ Set.univ
Tactic:
constructor
State after:
case refine_2.h.mp
x : ℝ
⊢ x ∈ ⋃₀ lower_intervals → x ∈ Set.univ

case refine_2.h.mpr
x : ℝ
⊢ x ∈ Set.univ → x ∈ ⋃₀ lower_intervals

State before:
case refine_2.h.mp
x : ℝ
⊢ x ∈ ⋃₀ lower_intervals → x ∈ Set.univ
Tactic:
aesop
State after:
no goals

State before:
case refine_2.h.mpr
x : ℝ
⊢ x ∈ Set.univ → x ∈ ⋃₀ lower_intervals
Tactic:
intro _
State after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ lower_intervals

State before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ ⋃₀ lower_intervals
Tactic:
apply Set.mem_sUnion.mpr
State after:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ lower_intervals, x ∈ t

State before:
case refine_2.h.mpr
x : ℝ
a✝ : x ∈ Set.univ
⊢ ∃ t ∈ lower_intervals, x ∈ t
Tactic:
use Set.Ico x (x+1)
State after:
case h
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ico x (x + 1) ∈ lower_intervals ∧ x ∈ Set.Ico x (x + 1)

State before:
case h
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ico x (x + 1) ∈ lower_intervals ∧ x ∈ Set.Ico x (x + 1)
Tactic:
constructor
State after:
case h.left
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ico x (x + 1) ∈ lower_intervals

case h.right
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ Set.Ico x (x + 1)

State before:
case h.left
x : ℝ
a✝ : x ∈ Set.univ
⊢ Set.Ico x (x + 1) ∈ lower_intervals
Tactic:
exact ⟨x, x+1, rfl⟩
State after:
no goals

State before:
case h.right
x : ℝ
a✝ : x ∈ Set.univ
⊢ x ∈ Set.Ico x (x + 1)
Tactic:
simp
State after:
no goals