coindep_iff_subset_compl_isBase — Mathlib

English

A set X is coindependent iff there exists a base B with B ⊆ E \ X and X ⊆ E.

Русский

Множество X коиндепендентно тогда и только тогда, существует база B с B ⊆ E \ X и X ⊆ E.

LaTeX

$$$ M.Coindep X \iff \exists B\, (M.IsBase B \land B \subseteq M.E \setminus X)\n\land X \subseteq M.E $$$

Lean4

theorem coindep_iff_subset_compl_isBase : M.Coindep X ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B :=
  by
  simp_rw [coindep_iff_exists', subset_diff]
  exact
    ⟨fun ⟨⟨B, hB, _, hBX⟩, hX⟩ ↦ ⟨B, hB, hX, hBX.symm⟩, fun ⟨B, hB, hXE, hXB⟩ ↦
      ⟨⟨B, hB, hB.subset_ground, hXB.symm⟩, hXE⟩⟩

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