[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
⊢ ∀ (r : R) (x : (fun x => LocallyConstant X Y) r),
    ↑(RingHom.comp constRingHom (algebraMap R Y)) r * x = x * ↑(RingHom.comp constRingHom (algebraMap R Y)) r
[PROOFSTEP]
intros
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
r✝ : R
x✝ : LocallyConstant X Y
⊢ ↑(RingHom.comp constRingHom (algebraMap R Y)) r✝ * x✝ = x✝ * ↑(RingHom.comp constRingHom (algebraMap R Y)) r✝
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
r✝ : R
x✝¹ : LocallyConstant X Y
x✝ : X
⊢ ↑(↑(RingHom.comp constRingHom (algebraMap R Y)) r✝ * x✝¹) x✝ =
    ↑(x✝¹ * ↑(RingHom.comp constRingHom (algebraMap R Y)) r✝) x✝
[PROOFSTEP]
exact Algebra.commutes' _ _
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
⊢ ∀ (r : R) (x : (fun x => LocallyConstant X Y) r), r • x = ↑(RingHom.comp constRingHom (algebraMap R Y)) r * x
[PROOFSTEP]
intros
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
r✝ : R
x✝ : LocallyConstant X Y
⊢ r✝ • x✝ = ↑(RingHom.comp constRingHom (algebraMap R Y)) r✝ * x✝
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
r✝ : R
x✝¹ : LocallyConstant X Y
x✝ : X
⊢ ↑(r✝ • x✝¹) x✝ = ↑(↑(RingHom.comp constRingHom (algebraMap R Y)) r✝ * x✝¹) x✝
[PROOFSTEP]
exact Algebra.smul_def' _ _
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
R : Type u_3
inst✝¹ : TopologicalSpace Y
Z : Type ?u.139413
inst✝ : Mul Z
f : X → Y
hf : Continuous f
r s : LocallyConstant Y Z
⊢ comap f (r * s) = comap f r * comap f s
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
R : Type u_3
inst✝¹ : TopologicalSpace Y
Z : Type ?u.139413
inst✝ : Mul Z
f : X → Y
hf : Continuous f
r s : LocallyConstant Y Z
x : X
⊢ ↑(comap f (r * s)) x = ↑(comap f r * comap f s) x
[PROOFSTEP]
simp [hf]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
R : Type u_3
inst✝¹ : TopologicalSpace Y
Z : Type ?u.141527
inst✝ : MulOneClass Z
f : X → Y
hf : Continuous f
⊢ comap f 1 = 1
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
R : Type u_3
inst✝¹ : TopologicalSpace Y
Z : Type ?u.141527
inst✝ : MulOneClass Z
f : X → Y
hf : Continuous f
x : X
⊢ ↑(comap f 1) x = ↑1 x
[PROOFSTEP]
simp [hf]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
R✝ : Type u_3
inst✝³ : TopologicalSpace Y
Z : Type ?u.147135
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : X → Y
hf : Continuous f
r : R
s : LocallyConstant Y Z
⊢ AddHom.toFun
      { toFun := comap f,
        map_add' :=
          (_ :
            ∀ (x y : LocallyConstant Y Z),
              ↑(comapAddMonoidHom f hf) (x + y) = ↑(comapAddMonoidHom f hf) x + ↑(comapAddMonoidHom f hf) y) }
      (r • s) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := comap f,
          map_add' :=
            (_ :
              ∀ (x y : LocallyConstant Y Z),
                ↑(comapAddMonoidHom f hf) (x + y) = ↑(comapAddMonoidHom f hf) x + ↑(comapAddMonoidHom f hf) y) }
        s
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
R✝ : Type u_3
inst✝³ : TopologicalSpace Y
Z : Type ?u.147135
R : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : X → Y
hf : Continuous f
r : R
s : LocallyConstant Y Z
x : X
⊢ ↑(AddHom.toFun
          { toFun := comap f,
            map_add' :=
              (_ :
                ∀ (x y : LocallyConstant Y Z),
                  ↑(comapAddMonoidHom f hf) (x + y) = ↑(comapAddMonoidHom f hf) x + ↑(comapAddMonoidHom f hf) y) }
          (r • s))
      x =
    ↑(↑(RingHom.id R) r •
          AddHom.toFun
            { toFun := comap f,
              map_add' :=
                (_ :
                  ∀ (x y : LocallyConstant Y Z),
                    ↑(comapAddMonoidHom f hf) (x + y) = ↑(comapAddMonoidHom f hf) x + ↑(comapAddMonoidHom f hf) y) }
            s)
      x
[PROOFSTEP]
simp [hf]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
R✝ : Type u_3
inst✝³ : TopologicalSpace Y
Z : Type ?u.155777
R : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring Z
inst✝ : Algebra R Z
f : X → Y
hf : Continuous f
r : R
⊢ OneHom.toFun (↑↑(comapRingHom f hf)) (↑(algebraMap R (LocallyConstant Y Z)) r) =
    ↑(algebraMap R (LocallyConstant X Z)) r
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
R✝ : Type u_3
inst✝³ : TopologicalSpace Y
Z : Type ?u.155777
R : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring Z
inst✝ : Algebra R Z
f : X → Y
hf : Continuous f
r : R
x : X
⊢ ↑(OneHom.toFun (↑↑(comapRingHom f hf)) (↑(algebraMap R (LocallyConstant Y Z)) r)) x =
    ↑(↑(algebraMap R (LocallyConstant X Z)) r) x
[PROOFSTEP]
simp [hf]


[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : TopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x => det (A x)
[PROOFSTEP]
simp_rw [Matrix.det_apply]
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : TopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x =>
    Finset.sum Finset.univ fun x_1 => ↑Equiv.Perm.sign x_1 • Finset.prod Finset.univ fun x_2 => A x (↑x_1 x_2) x_2
[PROOFSTEP]
refine' continuous_finset_sum _ fun l _ => Continuous.const_smul _ _
[GOAL]
X : Type u_1
α : Type u_2
l✝ : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l✝ → Type u_9
n' : l✝ → Type u_10
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : TopologicalRing R
A : X → Matrix n n R
hA : Continuous A
l : Equiv.Perm n
x✝ : l ∈ Finset.univ
⊢ Continuous fun x => Finset.prod Finset.univ fun x_1 => A x (↑l x_1) x_1
[PROOFSTEP]
refine' continuous_finset_prod _ fun l _ => hA.matrix_elem _ _
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
⊢ ∀ (i : n ⊕ p) (j : l ⊕ m), Continuous fun a => fromBlocks (A a) (B a) (C a) (D a) i j
[PROOFSTEP]
rintro (i | i) (j | j)
[GOAL]
case inl.inl
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : l
⊢ Continuous fun a => fromBlocks (A a) (B a) (C a) (D a) (Sum.inl i) (Sum.inl j)
[PROOFSTEP]
refine' Continuous.matrix_elem _ i j
[GOAL]
case inl.inr
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : m
⊢ Continuous fun a => fromBlocks (A a) (B a) (C a) (D a) (Sum.inl i) (Sum.inr j)
[PROOFSTEP]
refine' Continuous.matrix_elem _ i j
[GOAL]
case inr.inl
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : l
⊢ Continuous fun a => fromBlocks (A a) (B a) (C a) (D a) (Sum.inr i) (Sum.inl j)
[PROOFSTEP]
refine' Continuous.matrix_elem _ i j
[GOAL]
case inr.inr
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
⊢ Continuous fun a => fromBlocks (A a) (B a) (C a) (D a) (Sum.inr i) (Sum.inr j)
[PROOFSTEP]
refine' Continuous.matrix_elem _ i j
[GOAL]
case inl.inl
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : l
⊢ Continuous fun a => A a
[PROOFSTEP]
assumption
[GOAL]
case inl.inr
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : m
⊢ Continuous fun a => B a
[PROOFSTEP]
assumption
[GOAL]
case inr.inl
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : l
⊢ Continuous fun a => C a
[PROOFSTEP]
assumption
[GOAL]
case inr.inr
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
⊢ Continuous fun a => D a
[PROOFSTEP]
assumption
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
⊢ Continuous fun a => blockDiagonal' (A a) { fst := i₁, snd := i₂ } { fst := j₁, snd := j₂ }
[PROOFSTEP]
dsimp only [blockDiagonal'_apply']
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
⊢ Continuous fun a => if h : i₁ = j₁ then A a i₁ i₂ (cast (_ : n' j₁ = n' i₁) j₂) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
h : i₁ = j₁
⊢ Continuous fun a => A a i₁ i₂ (cast (_ : n' j₁ = n' i₁) j₂)
[PROOFSTEP]
subst h
[GOAL]
case pos
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₂ : n' i₁
⊢ Continuous fun a => A a i₁ i₂ (cast (_ : n' i₁ = n' i₁) j₂)
[PROOFSTEP]
exact ((continuous_apply i₁).comp hA).matrix_elem i₂ j₂
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
h : ¬i₁ = j₁
⊢ Continuous fun a => 0
[PROOFSTEP]
exact continuous_const
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
[PROOFSTEP]
exact hf.hasSum.matrix_transpose.tsum_eq.symm
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
[PROOFSTEP]
have hft := summable_matrix_transpose.not.mpr hf
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => (f x)ᵀ
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, transpose_zero]
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : Summable f
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ
[PROOFSTEP]
exact hf.hasSum.matrix_conjTranspose.tsum_eq.symm
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ
[PROOFSTEP]
have hft := summable_matrix_conjTranspose.not.mpr hf
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => (f x)ᴴ
⊢ (∑' (x : X), f x)ᴴ = ∑' (x : X), (f x)ᴴ
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, conjTranspose_zero]
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
[PROOFSTEP]
exact hf.hasSum.matrix_diagonal.tsum_eq.symm
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
[PROOFSTEP]
have hft := summable_matrix_diagonal.not.mpr hf
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal 0 = 0
[PROOFSTEP]
exact diagonal_zero
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
[PROOFSTEP]
exact hf.hasSum.matrix_blockDiagonal.tsum_eq.symm
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
[PROOFSTEP]
have hft := summable_matrix_blockDiagonal.not.mpr hf
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal 0 = 0
[PROOFSTEP]
exact blockDiagonal_zero
[GOAL]
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
[PROOFSTEP]
exact hf.hasSum.matrix_blockDiagonal'.tsum_eq.symm
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
[PROOFSTEP]
have hft := summable_matrix_blockDiagonal'.not.mpr hf
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), blockDiagonal' (f x)
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
[GOAL]
case neg
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq l
inst✝ : T2Space R
f : X → (i : l) → Matrix (m' i) (n' i) R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal' (f x)
⊢ blockDiagonal' 0 = 0
[PROOFSTEP]
exact blockDiagonal'_zero


[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
⊢ UpperSetTopology α
[PROOFSTEP]
letI := upperSetTopology' α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
this : TopologicalSpace α := upperSetTopology' α
⊢ UpperSetTopology α
[PROOFSTEP]
exact ⟨rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
⊢ LowerSetTopology α
[PROOFSTEP]
letI := lowerSetTopology' α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
this : TopologicalSpace α := lowerSetTopology' α
⊢ LowerSetTopology α
[PROOFSTEP]
exact ⟨rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : UpperSetTopology α
s : Set α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
⊢ instTopologicalSpaceOrderDual = lowerSetTopology' αᵒᵈ
[PROOFSTEP]
refine topologicalSpace_eq ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : UpperSetTopology α
s : Set α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
⊢ IsOpen = IsOpen
[PROOFSTEP]
rw [(UpperSetTopology.topology_eq (α))]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
⊢ WithUpperSetTopology.instTopologicalSpaceWithUpperSetTopology = induced (↑WithUpperSetTopology.ofUpperSet) inst✝¹
[PROOFSTEP]
erw [topology_eq α, induced_id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
⊢ WithUpperSetTopology.instTopologicalSpaceWithUpperSetTopology = upperSetTopology' α
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
⊢ IsOpen s ↔ IsUpperSet s
[PROOFSTEP]
rw [topology_eq α]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
⊢ IsOpen s ↔ IsUpperSet s
[PROOFSTEP]
rfl
  -- Alexandrov property, set formulation
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsOpen s
⊢ IsOpen (⋂₀ S)
[PROOFSTEP]
simp_rw [IsOpen_iff_IsUpperSet] at *
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsUpperSet s
⊢ IsUpperSet (⋂₀ S)
[PROOFSTEP]
apply isUpperSet_sInter
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsUpperSet s
⊢ ∀ (s : Set α), s ∈ S → IsUpperSet s
[PROOFSTEP]
intros s hs
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ : Set α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsUpperSet s
s : Set α
hs : s ∈ S
⊢ IsUpperSet s
[PROOFSTEP]
exact hf _ hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
ι : Sort u_3
f : ι → Set α
hf : ∀ (i : ι), IsOpen (f i)
⊢ IsOpen (⋂ (i : ι), f i)
[PROOFSTEP]
simp_rw [IsOpen_iff_IsUpperSet] at *
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
ι : Sort u_3
f : ι → Set α
hf : ∀ (i : ι), IsUpperSet (f i)
⊢ IsUpperSet (⋂ (i : ι), f i)
[PROOFSTEP]
apply isUpperSet_iInter
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
ι : Sort u_3
f : ι → Set α
hf : ∀ (i : ι), IsUpperSet (f i)
⊢ ∀ (i : ι), IsUpperSet (f i)
[PROOFSTEP]
intros i
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
ι : Sort u_3
f : ι → Set α
hf : ∀ (i : ι), IsUpperSet (f i)
i : ι
⊢ IsUpperSet (f i)
[PROOFSTEP]
exact hf i
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ IsClosed s ↔ IsLowerSet s
[PROOFSTEP]
rw [← isOpen_compl_iff, IsOpen_iff_IsUpperSet, isLowerSet_compl.symm, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ closure s = ↑(lowerClosure s)
[PROOFSTEP]
rw [subset_antisymm_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ closure s ⊆ ↑(lowerClosure s) ∧ ↑(lowerClosure s) ⊆ closure s
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ closure s ⊆ ↑(lowerClosure s)
[PROOFSTEP]
apply closure_minimal subset_lowerClosure _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ IsClosed ↑(lowerClosure s)
[PROOFSTEP]
rw [isClosed_iff_isLower]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ IsLowerSet ↑(lowerClosure s)
[PROOFSTEP]
exact LowerSet.lower (lowerClosure s)
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s✝ s : Set α
⊢ ↑(lowerClosure s) ⊆ closure s
[PROOFSTEP]
apply lowerClosure_min subset_closure (isClosed_isLower isClosed_closure)
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
a : α
⊢ closure {a} = Iic a
[PROOFSTEP]
rw [closure_eq_lowerClosure, lowerClosure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperSetTopology α
s : Set α
a : α
⊢ ↑(LowerSet.Iic a) = Iic a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
⊢ Monotone f ↔ Continuous f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
⊢ Monotone f → Continuous f
[PROOFSTEP]
intro hf
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Monotone f
⊢ Continuous f
[PROOFSTEP]
simp_rw [continuous_def, IsOpen_iff_IsUpperSet]
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsUpperSet s → IsUpperSet (f ⁻¹' s)
[PROOFSTEP]
exact fun _ hs ↦ IsUpperSet.preimage hs hf
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
⊢ Continuous f → Monotone f
[PROOFSTEP]
intro hf a b hab
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab : a ≤ b
⊢ f a ≤ f b
[PROOFSTEP]
rw [← mem_Iic, ← closure_singleton] at hab ⊢
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab✝ : a ∈ Iic b
hab : a ∈ closure {b}
⊢ f a ∈ closure {f b}
[PROOFSTEP]
apply (Continuous.closure_preimage_subset hf {f b})
[GOAL]
case mpr.a
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab✝ : a ∈ Iic b
hab : a ∈ closure {b}
⊢ a ∈ closure (f ⁻¹' {f b})
[PROOFSTEP]
apply mem_of_mem_of_subset hab
[GOAL]
case mpr.a
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab✝ : a ∈ Iic b
hab : a ∈ closure {b}
⊢ closure {b} ⊆ closure (f ⁻¹' {f b})
[PROOFSTEP]
apply closure_mono
[GOAL]
case mpr.a.h
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperSetTopology β
f : α → β
hf : Continuous f
a b : α
hab✝ : a ∈ Iic b
hab : a ∈ closure {b}
⊢ {b} ⊆ f ⁻¹' {f b}
[PROOFSTEP]
rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
⊢ Continuous f
[PROOFSTEP]
rw [continuous_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsOpen s → IsOpen (f ⁻¹' s)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)
[PROOFSTEP]
rw [IsOpen_iff_IsUpperSet]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen s
⊢ IsUpperSet (f ⁻¹' s)
[PROOFSTEP]
apply IsUpperSet.preimage _ hf
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : UpperSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : UpperTopology β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen s
⊢ IsUpperSet s
[PROOFSTEP]
apply UpperTopology.isUpperSet_of_isOpen hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
t₁ : TopologicalSpace α
inst✝¹ : UpperSetTopology α
t₂ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
hs : IsOpen s
⊢ IsOpen s
[PROOFSTEP]
rw [@IsOpen_iff_IsUpperSet α _ t₁]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
t₁ : TopologicalSpace α
inst✝¹ : UpperSetTopology α
t₂ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
hs : IsOpen s
⊢ IsUpperSet s
[PROOFSTEP]
exact UpperTopology.isUpperSet_of_isOpen hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : LowerSetTopology α
s : Set α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
⊢ instTopologicalSpaceOrderDual = upperSetTopology' αᵒᵈ
[PROOFSTEP]
refine topologicalSpace_eq ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : LowerSetTopology α
s : Set α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
⊢ IsOpen = IsOpen
[PROOFSTEP]
rw [(LowerSetTopology.topology_eq (α))]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
⊢ WithLowerSetTopology.instTopologicalSpaceWithLowerSetTopology = induced (↑WithLowerSetTopology.ofLowerSet) inst✝¹
[PROOFSTEP]
erw [topology_eq α, induced_id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
⊢ WithLowerSetTopology.instTopologicalSpaceWithLowerSetTopology = lowerSetTopology' α
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
⊢ IsOpen s ↔ IsLowerSet s
[PROOFSTEP]
rw [topology_eq α]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
⊢ IsOpen s ↔ IsLowerSet s
[PROOFSTEP]
rfl
  -- Alexandrov property, set formulation
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s✝ s : Set α
⊢ IsClosed s ↔ IsUpperSet s
[PROOFSTEP]
rw [← isOpen_compl_iff, IsOpen_iff_IsLowerSet, isUpperSet_compl.symm, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
a : α
⊢ closure {a} = Ici a
[PROOFSTEP]
rw [closure_eq_upperClosure, upperClosure_singleton]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerSetTopology α
s : Set α
a : α
⊢ ↑(UpperSet.Ici a) = Ici a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : LowerSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerSetTopology β
f : α → β
⊢ Monotone f ↔ Continuous f
[PROOFSTEP]
rw [← monotone_dual_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : LowerSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerSetTopology β
f : α → β
⊢ Monotone (↑toDual ∘ f ∘ ↑ofDual) ↔ Continuous f
[PROOFSTEP]
exact UpperSetTopology.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ) (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : LowerSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : α → β
hf : Monotone f
⊢ Continuous f
[PROOFSTEP]
apply
  UpperSetTopology.Monotone_to_UpperTopology_Continuous (α := αᵒᵈ) (β := βᵒᵈ) (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : LowerSetTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : α → β
hf : Monotone f
⊢ Monotone (↑toDual ∘ f ∘ ↑ofDual)
[PROOFSTEP]
exact Monotone.dual hf
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
t₁ : TopologicalSpace α
inst✝¹ : LowerSetTopology α
t₂ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
hs : IsOpen s
⊢ IsOpen s
[PROOFSTEP]
rw [@IsOpen_iff_IsLowerSet α _ t₁]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
t₁ : TopologicalSpace α
inst✝¹ : LowerSetTopology α
t₂ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
hs : IsOpen s
⊢ IsLowerSet s
[PROOFSTEP]
exact LowerTopology.isLowerSet_of_isOpen hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperSetTopology αᵒᵈ ↔ LowerSetTopology α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperSetTopology αᵒᵈ → LowerSetTopology α
[PROOFSTEP]
apply UpperSetTopology.instLowerSetTopologyDual
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerSetTopology α → UpperSetTopology αᵒᵈ
[PROOFSTEP]
apply LowerSetTopology.instUpperSetTopologyDual
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerSetTopology αᵒᵈ ↔ UpperSetTopology α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerSetTopology αᵒᵈ → UpperSetTopology α
[PROOFSTEP]
apply LowerSetTopology.instUpperSetTopologyDual
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperSetTopology α → LowerSetTopology αᵒᵈ
[PROOFSTEP]
apply UpperSetTopology.instLowerSetTopologyDual


[GOAL]
α : Type u
β : Type v
γ : Type w
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℝ
h : dist a✝ b✝ < ε
⊢ dist (-a✝) (-b✝) < ε
[PROOFSTEP]
rw [dist_comm] at h
[GOAL]
α : Type u
β : Type v
γ : Type w
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℝ
h : dist b✝ a✝ < ε
⊢ dist (-a✝) (-b✝) < ε
[PROOFSTEP]
simpa only [Real.dist_eq, neg_sub_neg] using h
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ TopologicalAddGroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
x r : ℝ
⊢ IsCompact (closedBall x r)
[PROOFSTEP]
rw [Real.closedBall_eq_Icc]
[GOAL]
α : Type u
β : Type v
γ : Type w
x r : ℝ
⊢ IsCompact (Icc (x - r) (x + r))
[PROOFSTEP]
apply isCompact_Icc
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ ∀ (u : Set ℝ), u ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b} → IsOpen u
[PROOFSTEP]
simp (config := { contextual := true }) [isOpen_Ioo]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
v : Set ℝ
hav : a ∈ v
hv : IsOpen v
l u : ℝ
hl : l < a
hu : a < u
h : Ioo l u ⊆ v
q : ℚ
hlq : l < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < u
⊢ Ioo ↑q ↑p ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}
[PROOFSTEP]
simp only [mem_iUnion]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
v : Set ℝ
hav : a ∈ v
hv : IsOpen v
l u : ℝ
hl : l < a
hu : a < u
h : Ioo l u ⊆ v
q : ℚ
hlq : l < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < u
⊢ ∃ i i_1 i_2, Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}
[PROOFSTEP]
exact ⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ cocompact ℝ = atBot ⊔ atTop
[PROOFSTEP]
simp only [← comap_dist_right_atTop_eq_cocompact (0 : ℝ), Real.dist_eq, sub_zero, comap_abs_atTop]
[GOAL]
α : Type u
β : Type v
γ : Type w
s : Set ℝ
x : ℝ
⊢ x ∈ closure s ↔ ∀ (ε : ℝ), ε > 0 → ∃ y, y ∈ s ∧ |y - x| < ε
[PROOFSTEP]
simp [mem_closure_iff_nhds_basis nhds_basis_ball, Real.dist_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ CompleteSpace ℝ
[PROOFSTEP]
apply complete_of_cauchySeq_tendsto
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
⊢ ∀ (u : ℕ → ℝ), CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
intro u hu
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
let c : CauSeq ℝ abs := ⟨u, Metric.cauchySeq_iff'.1 hu⟩
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
⊢ ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
refine' ⟨c.lim, fun s h => _⟩
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℝ
h : s ∈ 𝓝 (CauSeq.lim c)
⊢ s ∈ map u atTop
[PROOFSTEP]
rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
[GOAL]
case a.intro.intro
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℝ
h : s ∈ 𝓝 (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
⊢ s ∈ map u atTop
[PROOFSTEP]
have := c.equiv_lim ε ε0
[GOAL]
case a.intro.intro
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℝ
h : s ∈ 𝓝 (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
this : ∃ i, ∀ (j : ℕ), j ≥ i → |↑(c - CauSeq.const abs (CauSeq.lim c)) j| < ε
⊢ s ∈ map u atTop
[PROOFSTEP]
simp only [mem_map, mem_atTop_sets, mem_setOf_eq]
[GOAL]
case a.intro.intro
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℝ
h : s ∈ 𝓝 (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
this : ∃ i, ∀ (j : ℕ), j ≥ i → |↑(c - CauSeq.const abs (CauSeq.lim c)) j| < ε
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → b ∈ u ⁻¹' s
[PROOFSTEP]
refine' this.imp fun N hN n hn => hε (hN n hn)
[GOAL]
α : Type u
β : Type v
γ : Type w
x ε : ℝ
⊢ TotallyBounded (ball x ε)
[PROOFSTEP]
rw [Real.ball_eq_Ioo]
[GOAL]
α : Type u
β : Type v
γ : Type w
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))
[PROOFSTEP]
apply totallyBounded_Ioo
[GOAL]
α : Type u
β : Type v
γ : Type w
q : ℚ
x : ℝ
hx : x ∈ {r | ↑q ≤ r}
t : Set ℝ
ht : t ∈ 𝓝 x
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ t
p : ℚ
h₁ : x < ↑p
h₂ : ↑p < x + ε
⊢ ↑p ∈ ball x ε
[PROOFSTEP]
rwa [mem_ball, Real.dist_eq, abs_of_pos (sub_pos.2 h₁), sub_lt_iff_lt_add']
[GOAL]
α : Type u
β : Type v
γ : Type w
s : Set ℝ
⊢ Metric.Bounded s → BddBelow s ∧ BddAbove s
[PROOFSTEP]
intro bdd
[GOAL]
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
⊢ BddBelow s ∧ BddAbove s
[PROOFSTEP]
rcases(bounded_iff_subset_ball 0).1 bdd with
  ⟨r, hr⟩
    -- hr : s ⊆ closed_ball 0 r
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
r : ℝ
hr : s ⊆ closedBall 0 r
⊢ BddBelow s ∧ BddAbove s
[PROOFSTEP]
rw [Real.closedBall_eq_Icc] at hr
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
r : ℝ
hr : s ⊆ Icc (0 - r) (0 + r)
⊢ BddBelow s ∧ BddAbove s
[PROOFSTEP]
exact ⟨bddBelow_Icc.mono hr, bddAbove_Icc.mono hr⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous f
⊢ IsCompact (range f)
[PROOFSTEP]
rw [← hp.image_uIcc hc 0]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous f
⊢ IsCompact (f '' [[0, 0 + c]])
[PROOFSTEP]
exact isCompact_uIcc.image hf
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples a }
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples 0 }
[PROOFSTEP]
rw [AddSubgroup.zmultiples_zero_eq_bot]
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology { x // x ∈ ⊥ }
[PROOFSTEP]
exact Subsingleton.discreteTopology (α := (⊥ : Submodule ℤ ℝ))
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples a }
[PROOFSTEP]
rw [discreteTopology_iff_open_singleton_zero, isOpen_induced_iff]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = {0}
[PROOFSTEP]
refine' ⟨ball 0 |a|, isOpen_ball, _⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Subtype.val ⁻¹' ball 0 |a| = {0}
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case inr.h.mk
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
x : ℝ
hx : x ∈ AddSubgroup.zmultiples a
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' ball 0 |a| ↔ { val := x, property := hx } ∈ {0}
[PROOFSTEP]
obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
[GOAL]
case inr.h.mk.intro
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
k : ℤ
hx : k • a ∈ AddSubgroup.zmultiples a
⊢ { val := k • a, property := hx } ∈ Subtype.val ⁻¹' ball 0 |a| ↔ { val := k • a, property := hx } ∈ {0}
[PROOFSTEP]
simp [ha, Real.dist_eq, abs_mul, (by norm_cast : |(k : ℝ)| < 1 ↔ |k| < 1)]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
k : ℤ
hx : k • a ∈ AddSubgroup.zmultiples a
⊢ |↑k| < 1 ↔ |k| < 1
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ Tendsto Int.cast cofinite (cocompact ℝ)
[PROOFSTEP]
apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology { x // x ∈ AddMonoidHom.range (castAddHom ℝ) }
[PROOFSTEP]
rw [range_castAddHom]
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples 1 }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Tendsto (↑(↑(zmultiplesHom ℝ) a)) cofinite (cocompact ℝ)
[PROOFSTEP]
apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete $ smul_left_injective ℤ ha
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology { x // x ∈ AddMonoidHom.range (↑(zmultiplesHom ℝ) a) }
[PROOFSTEP]
rw [AddSubgroup.range_zmultiplesHom]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples a }
[PROOFSTEP]
infer_instance


[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
⊢ Associated (↑(Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
have hI := span_singleton_eq_bot.not.2 hf
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
⊢ Associated (↑(Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
let b' := ringBasis b (span { f }) hI
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated (↑(Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
classical
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']
let e := (b'.equiv ((span { f }).selfBasis b hI) <| Equiv.refl _).trans ((LinearEquiv.coord S S f hf).restrictScalars R)
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm
dsimp only [LinearEquiv.trans_apply]
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.comp_apply, ← LinearMap.ext_iff]
refine b'.ext fun i => ?_
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, Matrix.toLin_apply, Basis.repr_self,
  Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul, zero_smul, Finset.sum_ite_eq',
  mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]
change _ = f * _
rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply, LinearEquiv.coord_apply_smul, Ideal.selfBasis_def]
rfl
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated (↑(Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated (↑(Algebra.norm R) f)
    (↑LinearMap.det (↑(Matrix.toLin b' b') (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)))
[PROOFSTEP]
let e := (b'.equiv ((span { f }).selfBasis b hI) <| Equiv.refl _).trans ((LinearEquiv.coord S S f hf).restrictScalars R)
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
⊢ Associated (↑(Algebra.norm R) f)
    (↑LinearMap.det (↑(Matrix.toLin b' b') (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)))
[PROOFSTEP]
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
⊢ ∀ (x : S),
    ↑(↑(Matrix.toLin b' b') (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)) x =
      ↑(↑↑↑(Algebra.lmul R S) f) (↑e x)
[PROOFSTEP]
dsimp only [LinearEquiv.trans_apply]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
⊢ ∀ (x : S),
    ↑(↑(Matrix.toLin (ringBasis b (span {f}) hI) (ringBasis b (span {f}) hI))
            (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i))
        x =
      ↑(↑↑↑(Algebra.lmul R S) f)
        (↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
          (↑(Basis.equiv (ringBasis b (span {f}) hI) (selfBasis b (span {f}) hI) (Equiv.refl ι)) x))
[PROOFSTEP]
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.comp_apply, ← LinearMap.ext_iff]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
⊢ ↑↑(Matrix.toLin (ringBasis b (span {f}) hI) (ringBasis b (span {f}) hI))
      (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i) =
    LinearMap.comp (↑↑↑(Algebra.lmul R S) f)
      (LinearMap.comp ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ↑(Basis.equiv (ringBasis b (span {f}) hI) (selfBasis b (span {f}) hI) (Equiv.refl ι)))
[PROOFSTEP]
refine b'.ext fun i => ?_
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
i : ι
⊢ ↑(↑↑(Matrix.toLin (ringBasis b (span {f}) hI) (ringBasis b (span {f}) hI))
          (Matrix.diagonal fun i => smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i))
      (↑b' i) =
    ↑(LinearMap.comp (↑↑↑(Algebra.lmul R S) f)
          (LinearMap.comp ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
            ↑(Basis.equiv (ringBasis b (span {f}) hI) (selfBasis b (span {f}) hI) (Equiv.refl ι))))
      (↑b' i)
[PROOFSTEP]
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, Matrix.toLin_apply, Basis.repr_self,
  Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul, zero_smul, Finset.sum_ite_eq',
  mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
i : ι
⊢ smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i • ↑(ringBasis b (span {f}) hI) i =
    ↑(↑↑↑(Algebra.lmul R S) f)
      (↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) (↑(selfBasis b (span {f}) hI) (↑(Equiv.refl ι) i)))
[PROOFSTEP]
change _ = f * _
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
i : ι
⊢ smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i • ↑(ringBasis b (span {f}) hI) i =
    f * ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) (↑(selfBasis b (span {f}) hI) (↑(Equiv.refl ι) i))
[PROOFSTEP]
rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply, LinearEquiv.coord_apply_smul, Ideal.selfBasis_def]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : CommRing F
inst✝³ : Algebra F R
inst✝² : Algebra F S
inst✝¹ : IsScalarTower F R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  LinearEquiv.trans (Basis.equiv b' (selfBasis b (span {f}) hI) (Equiv.refl ι))
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
i : ι
⊢ smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i • ↑(ringBasis b (span {f}) hI) i =
    smithCoeffs b (span {f}) hI (↑(Equiv.refl ι) i) • ↑(ringBasis b (span {f}) hI) (↑(Equiv.refl ι) i)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
F : Type u_4
inst✝² : Field F
inst✝¹ : Algebra F[X] S
inst✝ : Finite ι
b : Basis ι F[X] S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ FiniteDimensional F (F[X] ⧸ span {smithCoeffs b I hI i})
[PROOFSTEP]
refine PowerBasis.finiteDimensional ?_
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
F : Type u_4
inst✝² : Field F
inst✝¹ : Algebra F[X] S
inst✝ : Finite ι
b : Basis ι F[X] S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ PowerBasis F (F[X] ⧸ span {smithCoeffs b I hI i})
[PROOFSTEP]
refine AdjoinRoot.powerBasis ?_
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
F : Type u_4
inst✝² : Field F
inst✝¹ : Algebra F[X] S
inst✝ : Finite ι
b : Basis ι F[X] S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ smithCoeffs b I hI i ≠ 0
[PROOFSTEP]
refine I.smithCoeffs_ne_zero b hI i
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
⊢ FiniteDimensional.finrank F (S ⧸ span {f}) = natDegree (↑(Algebra.norm F[X]) f)
[PROOFSTEP]
haveI := Fintype.ofFinite ι
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
⊢ FiniteDimensional.finrank F (S ⧸ span {f}) = natDegree (↑(Algebra.norm F[X]) f)
[PROOFSTEP]
have h := span_singleton_eq_bot.not.2 hf
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ FiniteDimensional.finrank F (S ⧸ span {f}) = natDegree (↑(Algebra.norm F[X]) f)
[PROOFSTEP]
rw [natDegree_eq_of_degree_eq (degree_eq_degree_of_associated <| associated_norm_prod_smith b hf)]
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ FiniteDimensional.finrank F (S ⧸ span {f}) = natDegree (∏ i : ι, smithCoeffs b (span {f}) (_ : ¬span {f} = ⊥) i)
[PROOFSTEP]
rw [natDegree_prod _ _ fun i _ => smithCoeffs_ne_zero b _ h i, finrank_quotient_eq_sum F h b]
  -- finrank_quotient_eq_sum slow
[GOAL]
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ ∑ i : ι, FiniteDimensional.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) =
    ∑ i : ι, natDegree (smithCoeffs b (span {f}) h i)
[PROOFSTEP]
congr with i
[GOAL]
case e_f.h
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsPrincipalIdealRing R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
i : ι
⊢ FiniteDimensional.finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) = natDegree (smithCoeffs b (span {f}) h i)
[PROOFSTEP]
exact (AdjoinRoot.powerBasis <| smithCoeffs_ne_zero b _ h i).finrank


[GOAL]
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace M
x : tsze R M
⊢ nhds x = Filter.prod (nhds (fst x)) (nhds (snd x))
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace M
fst✝ : R
snd✝ : M
⊢ nhds (fst✝, snd✝) = Filter.prod (nhds (fst (fst✝, snd✝))) (nhds (snd (fst✝, snd✝)))
[PROOFSTEP]
exact nhds_prod_eq


[GOAL]
α : Type u_1
⊢ Tendsto Real.toNNReal atTop atTop
[PROOFSTEP]
rw [← tendsto_coe_atTop]
[GOAL]
α : Type u_1
⊢ Tendsto (fun a => ↑(Real.toNNReal a)) atTop atTop
[PROOFSTEP]
exact tendsto_atTop_mono Real.le_coe_toNNReal tendsto_id
[GOAL]
α : Type u_1
⊢ ⨅ (l : ℝ≥0) (_ : ⊥ < l), 𝓟 (Set.Iio l) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Set.Iio a)
[PROOFSTEP]
simp only [bot_lt_iff_ne_bot]
[GOAL]
α : Type u_1
⊢ ⨅ (l : ℝ≥0) (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Set.Iio a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
[PROOFSTEP]
simp only [HasSum, ← coe_sum, tendsto_coe]
[GOAL]
α : Type u_1
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y
⊢ HasSum (fun x => Real.toNNReal (f x)) (Real.toNNReal y)
[PROOFSTEP]
lift y to ℝ≥0 using hy.nonneg hf₀
[GOAL]
case intro
α : Type u_1
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
y : ℝ≥0
hy : HasSum f ↑y
⊢ HasSum (fun x => Real.toNNReal (f x)) (Real.toNNReal ↑y)
[PROOFSTEP]
lift f to α → ℝ≥0 using hf₀
[GOAL]
case intro.intro
α : Type u_1
y : ℝ≥0
f : α → ℝ≥0
hy : HasSum (fun i => ↑(f i)) ↑y
⊢ HasSum (fun x => Real.toNNReal ((fun i => ↑(f i)) x)) (Real.toNNReal ↑y)
[PROOFSTEP]
simpa [hasSum_coe] using hy
[GOAL]
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) ↔ Summable f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
f : α → ℝ≥0
⊢ (Summable fun a => ↑(f a)) → Summable f
case mpr α : Type u_1 f : α → ℝ≥0 ⊢ Summable f → Summable fun a => ↑(f a)
[PROOFSTEP]
exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩
[GOAL]
case mpr
α : Type u_1
f : α → ℝ≥0
⊢ Summable f → Summable fun a => ↑(f a)
[PROOFSTEP]
exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩
[GOAL]
α : Type u_1
f : α → ℝ≥0
hf : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
[PROOFSTEP]
simp [tsum_def, hf, mt summable_coe.1 hf]
[GOAL]
α : Type u_1
a : ℝ≥0
f : α → ℝ≥0
⊢ ↑(∑' (x : α), a * f x) = ↑(a * ∑' (x : α), f x)
[PROOFSTEP]
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_left]
[GOAL]
α : Type u_1
f : α → ℝ≥0
a : ℝ≥0
⊢ ↑(∑' (x : α), f x * a) = ↑((∑' (x : α), f x) * a)
[PROOFSTEP]
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_right]
[GOAL]
α : Type u_1
β : Type u_2
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
⊢ Summable (f ∘ i)
[PROOFSTEP]
rw [← summable_coe] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a => ↑((f ∘ i) a)
[PROOFSTEP]
exact hf.comp_injective hi
[GOAL]
α : Type u_1
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun i => f (i + k)) ↔ Summable f
[PROOFSTEP]
rw [← summable_coe, ← summable_coe]
[GOAL]
α : Type u_1
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a => ↑(f (a + k))) ↔ Summable fun a => ↑(f a)
[PROOFSTEP]
exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k
[GOAL]
α : Type u_1
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i in Finset.range k, f i)
[PROOFSTEP]
rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]
[GOAL]
α : Type u_1
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => ↑(f n)) (↑a + ∑ i in Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i in Finset.range k, f i)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
f : α → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
[PROOFSTEP]
simp only [← summable_coe, ← tendsto_coe] at hf ⊢
[GOAL]
α : Type u_1
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
⊢ Tendsto (fun a => ↑(f a)) cofinite (𝓝 ↑0)
[PROOFSTEP]
exact hf.tendsto_cofinite_zero
[GOAL]
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f atTop (𝓝 0)
[PROOFSTEP]
rw [← Nat.cofinite_eq_atTop]
[GOAL]
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
[PROOFSTEP]
exact tendsto_cofinite_zero_of_summable hf
[GOAL]
α : Type u_1
f : α → ℝ≥0
⊢ Tendsto (fun s => ∑' (b : { x // ¬x ∈ s }), f ↑b) atTop (𝓝 0)
[PROOFSTEP]
simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]
[GOAL]
α : Type u_1
f : α → ℝ≥0
⊢ Tendsto (fun a => ∑' (a_1 : { x // ¬x ∈ a }), ↑(f ↑a_1)) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)
[GOAL]
n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun b => id b ^ n) atBot atBot
[PROOFSTEP]
simpa [OrderBot.atBot_eq, pos_iff_ne_zero]


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
f g : α →Co β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : α →Co β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ } =
    (fun f => f.toFun) g
⊢ { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
continuous_toFun✝¹ : Continuous { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, continuous_toFun := continuous_toFun✝¹ } =
    (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ }
⊢ { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, continuous_toFun := continuous_toFun✝¹ } =
    { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : β →Co γ
f₁ f₂ : α →Co β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]


[GOAL]
α : Type ?u.6639
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ WithLowerTopology.instTopologicalSpaceWithLowerTopology = induced (↑WithLowerTopology.ofLower) inst✝¹
[PROOFSTEP]
erw [topology_eq α, induced_id]
[GOAL]
α : Type ?u.6639
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ WithLowerTopology.instTopologicalSpaceWithLowerTopology = generateFrom {s | ∃ a, (Ici a)ᶜ = s}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
[PROOFSTEP]
rw [topology_eq α]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : Set.Finite s
⊢ IsClosed ↑(upperClosure s)
[PROOFSTEP]
simp only [← UpperSet.iInf_Ici, UpperSet.coe_iInf]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : Set.Finite s
⊢ IsClosed (⋃ (i : α) (_ : i ∈ s), ↑(UpperSet.Ici i))
[PROOFSTEP]
exact isClosed_biUnion h fun _ _ => isClosed_Ici
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : IsOpen s
⊢ IsLowerSet s
[PROOFSTEP]
replace h := isOpen_iff_generate_Ici_compl.1 h
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
h : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
⊢ IsLowerSet s
[PROOFSTEP]
induction h
[GOAL]
case basic
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ : Set α
a✝ : s✝ ∈ {t | ∃ a, (Ici a)ᶜ = t}
⊢ IsLowerSet s✝
case univ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
case inter
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u : Set α
h' : u ∈ {t | ∃ a, (Ici a)ᶜ = t}
⊢ IsLowerSet u
[PROOFSTEP]
case basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u : Set α
h' : u ∈ {t | ∃ a, (Ici a)ᶜ = t}
⊢ IsLowerSet u
[PROOFSTEP]
obtain ⟨a, rfl⟩ := h'
[GOAL]
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
a : α
⊢ IsLowerSet (Ici a)ᶜ
[PROOFSTEP]
exact (isUpperSet_Ici a).compl
[GOAL]
case univ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
case inter
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case univ => exact isLowerSet_univ
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
[PROOFSTEP]
case univ => exact isLowerSet_univ
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsLowerSet univ
[PROOFSTEP]
exact isLowerSet_univ
[GOAL]
case inter
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s s✝ t✝ : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s✝
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} t✝
a_ih✝¹ : IsLowerSet s✝
a_ih✝ : IsLowerSet t✝
⊢ IsLowerSet (s✝ ∩ t✝)
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case inter u v _ _ hu2 hv2 => exact hu2.inter hv2
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u v : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} u
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)
[PROOFSTEP]
case inter u v _ _ hu2 hv2 => exact hu2.inter hv2
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s u v : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} u
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)
[PROOFSTEP]
exact hu2.inter hv2
[GOAL]
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
a_ih✝ : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case sUnion _ _ ih => exact isLowerSet_sUnion ih
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
ih : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
case sUnion _ _ ih => exact isLowerSet_sUnion ih
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ (s : Set α), s ∈ S✝ → GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
ih : ∀ (s : Set α), s ∈ S✝ → IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)
[PROOFSTEP]
exact isLowerSet_sUnion ih
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsTopologicalBasis (lowerBasis α)
[PROOFSTEP]
convert isTopologicalBasis_of_subbasis (topology_eq α)
[GOAL]
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ lowerBasis α = (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]
[GOAL]
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s} =
    (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
ext s
[GOAL]
case h.e'_3.h
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s✝ s : Set α
⊢ s ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s} ↔
    s ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
constructor
[GOAL]
case h.e'_3.h.mp
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s✝ s : Set α
⊢ s ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s} →
    s ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
rintro ⟨F, hF, rfl⟩
[GOAL]
case h.e'_3.h.mp.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s F : Set α
hF : Set.Finite F
⊢ ⋂ (i : α) (_ : i ∈ F), (Ici i)ᶜ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
[PROOFSTEP]
refine' ⟨(fun a => (Ici a)ᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, _⟩
[GOAL]
case h.e'_3.h.mp.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s F : Set α
hF : Set.Finite F
⊢ (fun f => ⋂₀ f) ((fun a => (Ici a)ᶜ) '' F) = ⋂ (i : α) (_ : i ∈ F), (Ici i)ᶜ
[PROOFSTEP]
simp only [sInter_image]
[GOAL]
case h.e'_3.h.mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s✝ s : Set α
⊢ s ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}} →
    s ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
rintro ⟨F, ⟨hF, hs⟩, rfl⟩
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
haveI := hF.to_subtype
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
hs : F ⊆ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
rw [subset_def, Subtype.forall'] at hs
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
hs : ∀ (x : { a // a ∈ F }), ↑x ∈ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
choose f hf using hs
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
this : Finite ↑F
f : { a // a ∈ F } → α
hf : ∀ (x : { a // a ∈ F }), (Ici (f x))ᶜ = ↑x
⊢ (fun f => ⋂₀ f) F ∈ {s | ∃ t, Set.Finite t ∧ ⋂ (i : α) (_ : i ∈ t), (Ici i)ᶜ = s}
[PROOFSTEP]
exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
F : Set (Set α)
hF : Set.Finite F
this : Finite ↑F
f : { a // a ∈ F } → α
hf : ∀ (x : { a // a ∈ F }), (Ici (f x))ᶜ = ↑x
⊢ ⋂ (i : α) (_ : i ∈ range f), (Ici i)ᶜ = (fun f => ⋂₀ f) F
[PROOFSTEP]
simp_rw [biInter_range, hf, sInter_eq_iInter]
[GOAL]
α : Type u_2
inst✝³ : Preorder α
inst✝² : TopologicalSpace α
inst✝¹ : LowerTopology α
s : Set α
β : Type u_1
inst✝ : TopologicalSpace β
f : β → α
h : ∀ (a : α), IsClosed (f ⁻¹' Ici a)
⊢ Continuous f
[PROOFSTEP]
obtain rfl := LowerTopology.topology_eq α
[GOAL]
α : Type u_2
inst✝² : Preorder α
s : Set α
β : Type u_1
inst✝¹ : TopologicalSpace β
f : β → α
h : ∀ (a : α), IsClosed (f ⁻¹' Ici a)
inst✝ : LowerTopology α
⊢ Continuous f
[PROOFSTEP]
refine continuous_generateFrom ?_
[GOAL]
α : Type u_2
inst✝² : Preorder α
s : Set α
β : Type u_1
inst✝¹ : TopologicalSpace β
f : β → α
h : ∀ (a : α), IsClosed (f ⁻¹' Ici a)
inst✝ : LowerTopology α
⊢ ∀ (s : Set α), s ∈ {s | ∃ a, (Ici a)ᶜ = s} → IsOpen (f ⁻¹' s)
[PROOFSTEP]
rintro _ ⟨a, rfl⟩
[GOAL]
case intro
α : Type u_2
inst✝² : Preorder α
s : Set α
β : Type u_1
inst✝¹ : TopologicalSpace β
f : β → α
h : ∀ (a : α), IsClosed (f ⁻¹' Ici a)
inst✝ : LowerTopology α
a : α
⊢ IsOpen (f ⁻¹' (Ici a)ᶜ)
[PROOFSTEP]
exact (h a).isOpen_compl
[GOAL]
α : Type ?u.15319
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
x y : α
h : Inseparable x y
⊢ Ici x = Ici y
[PROOFSTEP]
simpa only [inseparable_iff_closure_eq, closure_singleton] using h
[GOAL]
α : Type ?u.16169
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
⊢ WithUpperTopology.instTopologicalSpaceWithUpperTopology = induced (↑WithUpperTopology.ofUpper) inst✝¹
[PROOFSTEP]
erw [topology_eq α, induced_id]
[GOAL]
α : Type ?u.16169
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
⊢ WithUpperTopology.instTopologicalSpaceWithUpperTopology = generateFrom {s | ∃ a, (Iic a)ᶜ = s}
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s
[PROOFSTEP]
rw [topology_eq α]
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : UpperTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
⊢ instTopologicalSpaceProd = generateFrom {s | ∃ a, (Ici a)ᶜ = s}
[PROOFSTEP]
refine' le_antisymm (le_generateFrom _) _
[GOAL]
case refine'_1
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
⊢ ∀ (s : Set (α × β)), s ∈ {s | ∃ a, (Ici a)ᶜ = s} → IsOpen s
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case refine'_1.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
x : α × β
⊢ IsOpen (Ici x)ᶜ
[PROOFSTEP]
exact (isClosed_Ici.prod isClosed_Ici).isOpen_compl
[GOAL]
case refine'_2
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
⊢ generateFrom {s | ∃ a, (Ici a)ᶜ = s} ≤ instTopologicalSpaceProd
[PROOFSTEP]
rw [(LowerTopology.isTopologicalBasis.prod LowerTopology.isTopologicalBasis).eq_generateFrom,
  le_generateFrom_iff_subset_isOpen, image2_subset_iff]
[GOAL]
case refine'_2
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
⊢ ∀ (x : Set α),
    x ∈ LowerTopology.lowerBasis α → ∀ (y : Set β), y ∈ LowerTopology.lowerBasis β → x ×ˢ y ∈ {s | IsOpen s}
[PROOFSTEP]
rintro _ ⟨s, hs, rfl⟩ _ ⟨t, ht, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
⊢ (↑(upperClosure s))ᶜ ×ˢ (↑(upperClosure t))ᶜ ∈ {s | IsOpen s}
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
⊢ IsOpen ((↑(upperClosure s))ᶜ ×ˢ (↑(upperClosure t))ᶜ)
[PROOFSTEP]
simp_rw [coe_upperClosure, compl_iUnion, prod_eq, preimage_iInter, preimage_compl]
  -- without `let`, `refine` tries to use the product topology and fails
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
⊢ IsOpen ((⋂ (i : α) (_ : i ∈ s), (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ (i : β) (_ : i ∈ t), (Prod.snd ⁻¹' Ici i)ᶜ)
[PROOFSTEP]
let _ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
⊢ IsOpen ((⋂ (i : α) (_ : i ∈ s), (Prod.fst ⁻¹' Ici i)ᶜ) ∩ ⋂ (i : β) (_ : i ∈ t), (Prod.snd ⁻¹' Ici i)ᶜ)
[PROOFSTEP]
refine (isOpen_biInter hs fun a _ => ?_).inter (isOpen_biInter ht fun b _ => ?_)
[GOAL]
case refine'_2.intro.intro.intro.intro.refine_1
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝¹ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
a : α
x✝ : a ∈ s
⊢ IsOpen (Prod.fst ⁻¹' Ici a)ᶜ
[PROOFSTEP]
exact GenerateOpen.basic _ ⟨(a, ⊥), by simp [Ici_prod_eq, prod_univ]⟩
[GOAL]
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝¹ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
a : α
x✝ : a ∈ s
⊢ (Ici (a, ⊥))ᶜ = (Prod.fst ⁻¹' Ici a)ᶜ
[PROOFSTEP]
simp [Ici_prod_eq, prod_univ]
[GOAL]
case refine'_2.intro.intro.intro.intro.refine_2
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝¹ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
b : β
x✝ : b ∈ t
⊢ IsOpen (Prod.snd ⁻¹' Ici b)ᶜ
[PROOFSTEP]
exact GenerateOpen.basic _ ⟨(⊥, b), by simp [Ici_prod_eq, univ_prod]⟩
[GOAL]
α : Type ?u.18877
β : Type ?u.18906
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LowerTopology α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : LowerTopology β
inst✝ : OrderBot β
s : Set α
hs : Set.Finite s
t : Set β
ht : Set.Finite t
x✝¹ : TopologicalSpace (α × β) := generateFrom {s | ∃ a, (Ici a)ᶜ = s}
b : β
x✝ : b ∈ t
⊢ (Ici (⊥, b))ᶜ = (Prod.snd ⁻¹' Ici b)ᶜ
[PROOFSTEP]
simp [Ici_prod_eq, univ_prod]
[GOAL]
α : Type ?u.24860
β : Type ?u.24889
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : UpperTopology α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : UpperTopology β
inst✝ : OrderTop β
⊢ instTopologicalSpaceProd = generateFrom {s | ∃ a, (Iic a)ᶜ = s}
[PROOFSTEP]
suffices : LowerTopology (α × β)ᵒᵈ
[GOAL]
α : Type ?u.24860
β : Type ?u.24889
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : UpperTopology α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : UpperTopology β
inst✝ : OrderTop β
this : LowerTopology (α × β)ᵒᵈ
⊢ instTopologicalSpaceProd = generateFrom {s | ∃ a, (Iic a)ᶜ = s}
[PROOFSTEP]
exact LowerTopology.topology_eq_lowerTopology (α := (α × β)ᵒᵈ)
[GOAL]
case this
α : Type ?u.24860
β : Type ?u.24889
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : UpperTopology α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : UpperTopology β
inst✝ : OrderTop β
⊢ LowerTopology (α × β)ᵒᵈ
[PROOFSTEP]
exact instLowerTopologyProd (α := αᵒᵈ) (β := βᵒᵈ)
[GOAL]
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
⊢ Continuous ↑f
[PROOFSTEP]
refine LowerTopology.continuous_of_Ici fun b => ?_
[GOAL]
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
⊢ IsClosed (↑f ⁻¹' Ici b)
[PROOFSTEP]
convert isClosed_Ici (a := sInf <| f ⁻¹' Ici b)
[GOAL]
case h.e'_3
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
⊢ ↑f ⁻¹' Ici b = Ici (sInf (↑f ⁻¹' Ici b))
[PROOFSTEP]
refine' Subset.antisymm (fun a => sInf_le) fun a ha => le_trans _ <| OrderHomClass.mono (f : α →o β) ha
[GOAL]
case h.e'_3
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (↑f ⁻¹' Ici b))
⊢ b ≤ ↑↑f (sInf (↑f ⁻¹' Ici b))
[PROOFSTEP]
refine' LE.le.trans _ (map_sInf f _).ge
[GOAL]
case h.e'_3
α : Type u_2
β : Type u_1
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : LowerTopology α
inst✝¹ : TopologicalSpace β
inst✝ : LowerTopology β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (↑f ⁻¹' Ici b))
⊢ b ≤ sInf (↑f '' (↑f ⁻¹' Ici b))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperTopology αᵒᵈ ↔ LowerTopology α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperTopology αᵒᵈ → LowerTopology α
[PROOFSTEP]
apply UpperTopology.instLowerTopologyDual
[GOAL]
case mpr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerTopology α → UpperTopology αᵒᵈ
[PROOFSTEP]
apply LowerTopology.instUpperTopologyDual
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerTopology αᵒᵈ ↔ UpperTopology α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ LowerTopology αᵒᵈ → UpperTopology α
[PROOFSTEP]
apply LowerTopology.instUpperTopologyDual
[GOAL]
case mpr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ UpperTopology α → LowerTopology αᵒᵈ
[PROOFSTEP]
apply UpperTopology.instLowerTopologyDual