notMem_mutuallySingularSetSlice — Mathlib

English

An x is not in the mutually singular slice κ η a if and only if rnDerivAux κ (κ+η) a x < 1.

Русский

Точка x не принадлежит срезу взаимной сингулярности κ η a тогда и только тогда, когда rnDerivAux κ (κ+η) a x < 1.

LaTeX

$$$x \notin \kappa.mutuallySingularSetSlice(\eta)(a) \iff rnDerivAux(\kappa, \kappa + \eta)(a, x) < 1$$$

Lean4

theorem notMem_mutuallySingularSetSlice (κ η : Kernel α γ) (a : α) (x : γ) :
    x ∉ mutuallySingularSetSlice κ η a ↔ rnDerivAux κ (κ + η) a x < 1 := by simp [mutuallySingularSetSlice]

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