exists_insert_of_encard_lt — Mathlib

English

If I and J are independent and I.encard < J.encard, there exists e ∈ J \\ I such that I ∪ {e} is independent.

Русский

Если I и J независимы и encard(I) < encard(J), существует e ∈ J \\ I, такое что I ∪ {e} независимо.

LaTeX

$$If $I,J$ are independent and $I.encard < J.encard$, then there exists $e \\in J \\setminus I$ with $M.Indep(I \\cup \\{e\\})$.$$

Lean4

theorem exists_insert_of_encard_lt {I J : Set α} (hI : M.Indep I) (hJ : M.Indep J) (hcard : I.encard < J.encard) :
    ∃ e ∈ J \ I, M.Indep (insert e I) :=
  augment hI hJ hcard

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