Humer

Komentarz

• rdr

  13:57 edytowano 14:01

  Tak wygląda ,,certyfikat" dla głupiej reguły de l'Hospitala w Lean, brr.... (dokładniej: odwołanie się do twierdzenia z Mathlib)

  import Mathlib.Analysis.Calculus.LHopital

  open Filter Set

  theorem lhopital_certificate
  {a L : ℝ}
  {f f' g g' : ℝ → ℝ}
  (hf' :
  ∀ᶠ x in nhds a, HasDerivAt f (f' x) x)
  (hg' :
  ∀ᶠ x in nhds a, HasDerivAt g (g' x) x)
  (hg'_ne :
  ∀ᶠ x in nhds a, g' x ≠ 0)
  (hf0 :
  Tendsto f (nhds a) (nhds 0))
  (hg0 :
  Tendsto g (nhds a) (nhds 0))
  (hderiv :
  Tendsto (fun x => f' x / g' x)
  (nhds a) (nhds L)) :
  Tendsto (fun x => f x / g x)
  (nhdsWithin a {a}ᶜ) (nhds L) := by
  exact HasDerivAt.lhopital_zero_nhds
  hf' hg' hg'_ne hf0 hg0 hderiv

  EDIT: forum nie ma wsparcie dla kodu w Markdown'ie

  0
• Wielen

  15:32

  To ma być humer?

  0