mem_indepSetFinset_iff — Mathlib

English

An n-independent set belongs to indepSetFinset n if and only if it is an n-independent set.

Русский

Подмножество является n-независимым множеством тогда и только тогда, когда принадлежит indepSetFinset n.

LaTeX

$$$s \\in G.indepSetFinset(n) \\iff G.IsNIndepSet(n,s)$$$

Lean4

@[simp]
theorem mem_indepSetFinset_iff : s ∈ G.indepSetFinset n ↔ G.IsNIndepSet n s :=
  mem_filter.trans <| and_iff_right <| mem_univ _

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