dual_dep_iff_forall — Mathlib

English

The dual Dep I relation satisfies: (M✶.Dep I) ↔ (∀ B, M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E.

Русский

Дугая зависимость дуала удовлетворяет: (M✶.Dep I) эквивалентно ∀ B базис M, I ∩ B непусто и I ⊆ M.E.

LaTeX

$$(M✶.Dep I) ↔ ((∀ B, M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E)$$

Lean4

theorem dual_dep_iff_forall : (M✶.Dep I) ↔ (∀ B, M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E := by
  simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and, not_exists, not_and,
    not_disjoint_iff_nonempty_inter, Classical.imp_iff_right_iff, iff_true_intro Or.inl]

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