internlm/Lean-Github huggingface dataset:
Theorem: SciLean.IsContinuousLinearMap.ite.arg_te.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.246592
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.246598
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.246632
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.246664
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.246670
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.246704
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.246736
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.246768
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.246776
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.246900
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.246933
inst✝³ : Fintype ι
E : ι → Type ?u.246941
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsContinuousLinearMap R t
he : IsContinuousLinearMap R e
h : c
⊢ IsContinuousLinearMap R fun x => t x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.ite.arg_te.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.246592
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.246598
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.246632
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.246664
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.246670
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.246704
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.246736
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.246768
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.246776
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.246900
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.246933
inst✝³ : Fintype ι
E : ι → Type ?u.246941
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsContinuousLinearMap R t
he : IsContinuousLinearMap R e
h : ¬c
⊢ IsContinuousLinearMap R fun x => if c then t x else e x
Tactic:
simp[h]
Proof state after:
R✝¹ : Type ?u.246592
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.246598
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.246632
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.246664
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.246670
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.246704
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.246736
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.246768
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.246776
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.246900
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.246933
inst✝³ : Fintype ι
E : ι → Type ?u.246941
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsContinuousLinearMap R t
he : IsContinuousLinearMap R e
h : ¬c
⊢ IsContinuousLinearMap R fun x => e x
Theorem: SciLean.IsContinuousLinearMap.ite.arg_te.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.246592
inst✝³⁴ : Semiring R✝¹
X✝¹ : Type ?u.246598
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.246632
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝¹ Y✝¹
R✝ : Type ?u.246664
inst✝²⁷ : Semiring R✝
X✝ : Type ?u.246670
inst✝²⁶ : TopologicalSpace X✝
inst✝²⁵ : AddCommMonoid X✝
inst✝²⁴ : Module R✝ X✝
Y✝ : Type ?u.246704
inst✝²³ : TopologicalSpace Y✝
inst✝²² : AddCommMonoid Y✝
inst✝²¹ : Module R✝ Y✝
Z✝ : Type ?u.246736
inst✝²⁰ : TopologicalSpace Z✝
inst✝¹⁹ : AddCommMonoid Z✝
inst✝¹⁸ : Module R✝ Z✝
ι✝ : Type ?u.246768
inst✝¹⁷ : Fintype ι✝
E✝ : ι✝ → Type ?u.246776
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.246900
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.246933
inst✝³ : Fintype ι
E : ι → Type ?u.246941
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
c : Prop
t e : X → Y
ht : IsContinuousLinearMap R t
he : IsContinuousLinearMap R e
h : ¬c
⊢ IsContinuousLinearMap R fun x => e x
Tactic:
fun_prop
Proof state after:
no goals
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
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
Tactic:
case isTrue h  => simp[h]; apply ht
Proof state after:
no goals
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
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
Tactic:
case isFalse h => simp[h]; apply he
Proof state after:
no goals
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
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
Tactic:
simp[h]
Proof state after:
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 => t ⋯ x
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
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 => t ⋯ x
Tactic:
apply ht
Proof state after:
no goals
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
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
Tactic:
simp[h]
Proof state after:
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 => e ⋯ x
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
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 => e ⋯ x
Tactic:
apply he
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.isContinuousLinearMap_differentiable
Proof state before:
R✝¹ : Type ?u.248959
inst✝³⁹ : Semiring R✝¹
X✝² : Type ?u.248965
inst✝³⁸ : TopologicalSpace X✝²
inst✝³⁷ : AddCommMonoid X✝²
inst✝³⁶ : Module R✝¹ X✝²
Y✝² : Type ?u.248999
inst✝³⁵ : TopologicalSpace Y✝²
inst✝³⁴ : AddCommMonoid Y✝²
inst✝³³ : Module R✝¹ Y✝²
R✝ : Type ?u.249031
inst✝³² : Semiring R✝
X✝¹ : Type ?u.249037
inst✝³¹ : TopologicalSpace X✝¹
inst✝³⁰ : AddCommMonoid X✝¹
inst✝²⁹ : Module R✝ X✝¹
Y✝¹ : Type ?u.249071
inst✝²⁸ : TopologicalSpace Y✝¹
inst✝²⁷ : AddCommMonoid Y✝¹
inst✝²⁶ : Module R✝ Y✝¹
Z✝ : Type ?u.249103
inst✝²⁵ : TopologicalSpace Z✝
inst✝²⁴ : AddCommMonoid Z✝
inst✝²³ : Module R✝ Z✝
ι✝ : Type ?u.249135
inst✝²² : Fintype ι✝
E✝ : ι✝ → Type ?u.249143
inst✝²¹ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²⁰ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.249193
inst✝¹⁸ : Semiring R
X✝ : Type ?u.249199
inst✝¹⁷ : TopologicalSpace X✝
inst✝¹⁶ : AddCommMonoid X✝
inst✝¹⁵ : Module R X✝
Y✝ : Type ?u.249234
inst✝¹⁴ : TopologicalSpace Y✝
inst✝¹³ : AddCommMonoid Y✝
inst✝¹² : Module R Y✝
Z : Type ?u.249267
inst✝¹¹ : TopologicalSpace Z
inst✝¹⁰ : AddCommMonoid Z
inst✝⁹ : Module R Z
ι : Type ?u.249300
inst✝⁸ : Fintype ι
E : ι → Type ?u.249308
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommMonoid (E i)
inst✝⁵ : (i : ι) → Module R (E i)
K : Type u_1
inst✝⁴ : RCLike K
X : Type u_2
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace K X
Y : Type u_3
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace K Y
f : X → Y
hf this : IsContinuousLinearMap K f
⊢ Differentiable K f
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.Inner.inner.arg_a0.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.254503
inst✝⁴¹ : Semiring R✝¹
X✝² : Type ?u.254509
inst✝⁴⁰ : TopologicalSpace X✝²
inst✝³⁹ : AddCommMonoid X✝²
inst✝³⁸ : Module R✝¹ X✝²
Y✝² : Type ?u.254543
inst✝³⁷ : TopologicalSpace Y✝²
inst✝³⁶ : AddCommMonoid Y✝²
inst✝³⁵ : Module R✝¹ Y✝²
R✝ : Type ?u.254575
inst✝³⁴ : Semiring R✝
X✝¹ : Type ?u.254581
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝ X✝¹
Y✝¹ : Type ?u.254615
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝ Y✝¹
Z✝ : Type ?u.254647
inst✝²⁷ : TopologicalSpace Z✝
inst✝²⁶ : AddCommMonoid Z✝
inst✝²⁵ : Module R✝ Z✝
ι✝ : Type ?u.254679
inst✝²⁴ : Fintype ι✝
E✝ : ι✝ → Type ?u.254687
inst✝²³ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²² : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²¹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.254737
inst✝²⁰ : Semiring R
X✝ : Type ?u.254743
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R X✝
Y✝ : Type ?u.254778
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R Y✝
Z : Type ?u.254811
inst✝¹³ : TopologicalSpace Z
inst✝¹² : AddCommMonoid Z
inst✝¹¹ : Module R Z
ι : Type ?u.254844
inst✝¹⁰ : Fintype ι
E : ι → Type ?u.254852
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommMonoid (E i)
inst✝⁷ : (i : ι) → Module R (E i)
K : Type u_1
inst✝⁶ : RCLike K
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module K X
Y : Type u_3
inst✝² : NormedAddCommGroup Y
inst✝¹ : InnerProductSpace K Y
inst✝ : CompleteSpace Y
f : X → Y
x✝ : IsContinuousLinearMap K f
y : Y
⊢ IsContinuousLinearMap K fun x => ⟪f x, y⟫_K
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.IsContinuousLinearMap.Inner.inner.arg_a1.IsContinuousLinearMap_rule
Proof state before:
R✝¹ : Type ?u.258319
inst✝⁴¹ : Semiring R✝¹
X✝² : Type ?u.258325
inst✝⁴⁰ : TopologicalSpace X✝²
inst✝³⁹ : AddCommMonoid X✝²
inst✝³⁸ : Module R✝¹ X✝²
Y✝² : Type ?u.258359
inst✝³⁷ : TopologicalSpace Y✝²
inst✝³⁶ : AddCommMonoid Y✝²
inst✝³⁵ : Module R✝¹ Y✝²
R✝ : Type ?u.258391
inst✝³⁴ : Semiring R✝
X✝¹ : Type ?u.258397
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝ X✝¹
Y✝¹ : Type ?u.258431
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝ Y✝¹
Z✝ : Type ?u.258463
inst✝²⁷ : TopologicalSpace Z✝
inst✝²⁶ : AddCommMonoid Z✝
inst✝²⁵ : Module R✝ Z✝
ι✝ : Type ?u.258495
inst✝²⁴ : Fintype ι✝
E✝ : ι✝ → Type ?u.258503
inst✝²³ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²² : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²¹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.258553
inst✝²⁰ : Semiring R
X✝ : Type ?u.258559
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R X✝
Y✝ : Type ?u.258594
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R Y✝
Z : Type ?u.258627
inst✝¹³ : TopologicalSpace Z
inst✝¹² : AddCommMonoid Z
inst✝¹¹ : Module R Z
ι : Type ?u.258660
inst✝¹⁰ : Fintype ι
E : ι → Type ?u.258668
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommMonoid (E i)
inst✝⁷ : (i : ι) → Module R (E i)
K : Type u_1
inst✝⁶ : RCLike K
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module K X
Y : Type u_3
inst✝² : NormedAddCommGroup Y
inst✝¹ : InnerProductSpace K Y
inst✝ : CompleteSpace Y
f : X → Y
x✝ : IsContinuousLinearMap K f
y : Y
⊢ IsContinuousLinearMap K fun x => ⟪y, f x⟫_K
Tactic:
sorry_proof
Proof state after:
no goals