mem_nonDegenerate_iff — Mathlib

English

For a subcomplex A, membership in A’s non-degenerate set agrees with membership in X’s non-degenerate set.

Русский

Принадлежность A non-degenerate согласуется с принадлежностью X non-degenerate.

LaTeX

$$$ x \in A_{\text{nonDegenerate}}(n) \iff x.\mathrm{val} \in X_{\text{nonDegenerate}}(n) $$$

Lean4

theorem mem_nonDegenerate_iff {n : ℕ} (x : A.obj (op ⦋n⦌)) : x ∈ nonDegenerate A n ↔ x.val ∈ X.nonDegenerate n := by
  rw [mem_nonDegenerate_iff_notMem_degenerate, mem_nonDegenerate_iff_notMem_degenerate, mem_degenerate_iff]

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