Theorem: SciLean.IsContinuousLinearMap.dite.arg_te.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.247422
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.247428
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.247462
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.247494
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.247500
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.247534
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.247566
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.247598
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.247606
inst✝¹⁶ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁵ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁴ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_1
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_3
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.247730
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.247763
inst✝³ : Fintype ι
E : ι → Type ?u.247771
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
dec : Decidable c
t : c → X → Y
ht : ∀ (p : c), IsContinuousLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsContinuousLinearMap R (e p)
⊢ IsContinuousLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x
Tactic:
induction dec
Proof state after:
case isFalse
R✝¹ : Type ?u.247422
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.247428
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.247462
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.247494
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.247500
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.247534
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.247566
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.247598
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.247606
inst✝¹⁶ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁵ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁴ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_1
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_3
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.247730
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.247763
inst✝³ : Fintype ι
E : ι → Type ?u.247771
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsContinuousLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsContinuousLinearMap R (e p)
h✝ : ¬c
⊢ IsContinuousLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x

case isTrue
R✝¹ : Type ?u.247422
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.247428
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.247462
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.247494
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.247500
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.247534
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.247566
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.247598
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.247606
inst✝¹⁶ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁵ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁴ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_1
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_3
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type ?u.247730
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.247763
inst✝³ : Fintype ι
E : ι → Type ?u.247771
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t : c → X → Y
ht : ∀ (p : c), IsContinuousLinearMap R (t p)
e : ¬c → X → Y
he : ∀ (p : ¬c), IsContinuousLinearMap R (e p)
h✝ : c
⊢ IsContinuousLinearMap R fun x => if x_1 : c then t x_1 x else e x_1 x