coindep_iff_exists' — Mathlib

English

A set X is coindependent in M iff there exists a base B with B ⊆ E \ X and X ⊆ E, i.e., a base disjoint from X contained in the ground, together with X contained in the ground.

Русский

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

LaTeX

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

Lean4

theorem coindep_iff_exists' : M.Coindep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E :=
  by
  simp_rw [Coindep, dual_indep_iff_exists', and_comm (a := _ ⊆ _), and_congr_left_iff, subset_diff]
  exact fun _ ↦ ⟨fun ⟨B, hB, hXB⟩ ↦ ⟨B, hB, hB.subset_ground, hXB.symm⟩, fun ⟨B, hB, _, hBX⟩ ↦ ⟨B, hB, hBX.symm⟩⟩

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