mem_closure_iff' — Mathlib

English

For an independent I, x ∈ cl(I) if and only if x ∈ E and (I ∪ {x} independent implies x ∈ I).

Русский

Пусть I независим; тогда x ∈ cl(I) если и только если x ∈ E и (I ∪ {x} независимо → x ∈ I).

LaTeX

$$$x \in E \wedge (\operatorname{Indep}(I \cup \{x\}) \rightarrow x \in I) \iff x \in \operatorname{cl}(I)$$$

Lean4

theorem mem_closure_iff' (hI : M.Indep I) : x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I) :=
  by
  rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground, imp_iff_not_or]
  have := hI.subset_ground
  aesop

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