mem_nonDegenerate_iff_notMem_degenerate

English

For every x in X_n, x is non-degenerate iff x is not in the degenerate set.

Русский

Для каждого x в X_n верно: x недегенеративен тогда и только тогда, когда x не лежит в множестве дегenerate.

LaTeX

$$$ x \in X_{\text{nonDegenerate}}(n) \;\iff\; x \notin X_{\text{degenerate}}(n) $$$

Lean4

theorem mem_nonDegenerate_iff_notMem_degenerate (x : X _⦋n⦌) : x ∈ X.nonDegenerate n ↔ x ∉ X.degenerate n :=
  Iff.rfl

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