X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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
X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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₂ }
dsimp only [blockDiagonal'_apply']
case inl
X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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₂)

case inr
X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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
X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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
split_ifs with h
case inl
X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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₂)
case inl
X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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₂)
subst h
no goals
case inl
X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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₂)
exact ((continuous_apply i₁).comp hA).matrix_elem i₂ j₂
no goals
case inr
X : Type u_5
α : Type ?u.39277
l : Type u_2
m : Type ?u.39283
n : Type ?u.39286
p : Type ?u.39289
S : Type ?u.39292
R : Type u_1
m' : l → Type u_3
n' : l → Type u_4
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
exact continuous_const