rnDeriv_eq_top_iff' — Mathlib

English

The infinite value of rnDeriv κ η a x is characterized by x belonging to the slice of mutual singularity at a.

Русский

Бесконечность rnDeriv κ η a x характеризуется тем, что x принадлежит срезу взаимной сингулярности при a.

LaTeX

$$$ rnDeriv(\kappa, \eta)\ a\ x = \infty \iff x \in \text{mutuallySingularSetSlice}(\kappa, \eta)(a)$$$

Lean4

theorem rnDeriv_eq_top_iff' (κ η : Kernel α γ) (a : α) (x : γ) :
    rnDeriv κ η a x = ∞ ↔ x ∈ mutuallySingularSetSlice κ η a := by
  rw [rnDeriv_eq_top_iff, mutuallySingularSet, mutuallySingularSetSlice, mem_setOf, mem_setOf]

Похожие утверждения