Theorem: DiracSeq.support (ForML/Dirac.lean)

State before:
b : ℝ
hb : b ≠ 0
⊢ Function.support (DiracSeq b) = Set.univ
Tactic:
simp [DiracSeq.def]
State after:
b : ℝ
hb : b ≠ 0
⊢ (((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩ Function.support fun x => rexp (-(b * x) ^ 2)) =
    Set.univ

State before:
b : ℝ
hb : b ≠ 0
⊢ (((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩ Function.support fun x => rexp (-(b * x) ^ 2)) =
    Set.univ
Tactic:
ext x
State after:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ (x ∈
      ((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩
        Function.support fun x => rexp (-(b * x) ^ 2)) ↔
    x ∈ Set.univ

State before:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ (x ∈
      ((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩
        Function.support fun x => rexp (-(b * x) ^ 2)) ↔
    x ∈ Set.univ
Tactic:
simp [hb, sqrt_pi_pos.ne']
State after:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ ¬rexp (-(b * x) ^ 2) = 0

State before:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ ¬rexp (-(b * x) ^ 2) = 0
Tactic:
rw [← ne_eq]
State after:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ rexp (-(b * x) ^ 2) ≠ 0

State before:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ rexp (-(b * x) ^ 2) ≠ 0
Tactic:
exact ne_of_gt (exp_pos _)
State after:
no goals