indep_iff_forall_notMem_closure_diff'

English

M.Indep I is equivalent to I ⊆ E and ∀ e∈I, e ∉ closure(I\{e}).

Русский

M.Indep I эквивалентно I ⊆ E и ∀ e∈I, e ∉ closure(I\{e}).

LaTeX

$$$M.Indep I \iff (I \subseteq M.E) \land \forall e \in I, e \notin M.closure(I\setminus\{e\})$$$

Lean4

/-- An alternative version of `Matroid.indep_iff_forall_notMem_closure_diff` where the
hypothesis that `I ⊆ M.E` is contained in the RHS rather than the hypothesis. -/
theorem indep_iff_forall_notMem_closure_diff' : M.Indep I ↔ I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ { e }) :=
  ⟨fun h ↦ ⟨h.subset_ground, (indep_iff_forall_notMem_closure_diff h.subset_ground).mp h⟩, fun h ↦
    (indep_iff_forall_notMem_closure_diff h.1).mpr h.2⟩

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