indep_iff_not_dep — Mathlib

English

Independence is equivalent to not being dependent together with being contained in E.

Русский

Независимость эквивалентна не-зависимости и принадлежности к E.

LaTeX

$$$ M.Indep I \iff (\neg M.Dep I \land I \subseteq M.E) $$$

Lean4

theorem indep_iff_not_dep : M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E :=
  by
  rw [dep_iff, not_and, not_imp_not]
  exact ⟨fun h ↦ ⟨fun _ ↦ h, h.subset_ground⟩, fun h ↦ h.1 h.2⟩

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