Komentarz

• rdr

  9 September edytowano 9 September

  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

  9 September

  To ma być humer?

  1
• Eden

  9 September

  @Wielen powiedział(a):
  To ma być humer?

  Kulega nie ma poczucia humera?

  0
• Wielen

  9 September

  Nie mnie oceniać.

  0
• Mordechlaj_Mashke

  00:22

  Humer to jest A odwrócone do góry nogamy.
  Czego nie rozumisz?

  👣

  🐾
  🐾

  1
• Wielen

  06:16

  Czy ja jestem Eskimosem żeby wszystko rozumić ?

  0
• ms.wygnaniec

  06:35

  @Wielen powiedział(a):
  Czy ja jestem Eskimosem żeby wszystko rozumić ?

  To jak dowcip informatyczny:

  • jakiej maski potrzebujesz, żeby nikt Cię nie widział?
  • 255.255.255.255

  0