rnDeriv_eq_top_iff — Mathlib

English

The equality rnDeriv κ η a x = ∞ holds if and only if (a,x) lies in the mutual singular set κ η.

Русский

Уравнение rnDeriv κ η a x = ∞ верно тогда и только тогда, когда (a,x) принадлежит множеству взаимной сингулярности κ η.

LaTeX

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

Lean4

theorem rnDeriv_eq_top_iff (κ η : Kernel α γ) (a : α) (x : γ) :
    rnDeriv κ η a x = ∞ ↔ (a, x) ∈ mutuallySingularSet κ η :=
  by
  simp only [rnDeriv, ENNReal.div_eq_top, ne_eq, ENNReal.ofReal_eq_zero, not_le, tsub_le_iff_right, zero_add,
    ENNReal.ofReal_ne_top, not_false_eq_true, and_true, or_false, mutuallySingularSet, mem_setOf_eq,
    and_iff_right_iff_imp]
  exact fun h ↦ zero_lt_one.trans_le h

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