mem_mutuallySingularSetSlice — Mathlib

English

For any a and x, x belongs to the mutually singular slice κ η a exactly when 1 ≤ rnDerivAux κ (κ+η) a x.

Русский

Для любых a и x принадлежность x к срезу взаимной сингулярности κ η a эквивалентна 1 ≤ rnDerivAux κ (κ+η) a x.

LaTeX

$$$x \in \kappa.mutuallySingularSetSlice(\eta)(a) \iff 1 \le \mathrm{rnDerivAux}(\kappa, \kappa + \eta)(a, x)$$$

Lean4

theorem mem_mutuallySingularSetSlice (κ η : Kernel α γ) (a : α) (x : γ) :
    x ∈ mutuallySingularSetSlice κ η a ↔ 1 ≤ rnDerivAux κ (κ + η) a x := by rw [mutuallySingularSetSlice, mem_setOf]

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