closure_eq_closure_of_subset_of_forall_insert

English

If X is finite, X ⊆ Y, and for every e in Y \ X we have eRk(insert e X) ≤ eRk X, then the closures of X and Y coincide: cl(X) = cl(Y).

Русский

Если X конечно, X ⊆ Y и для каждого e в Y \ X выполняется eRk(Insert e X) ≤ eRk X, то closures одинаковы: cl(X) = cl(Y).

LaTeX

$$If $M$ is a matroid, $X,Y\\subseteq A$, with $X\\subseteq Y$, $X$ finite, and $\\forall e\\in Y\\setminus X$, $M.eRk(\\mathrm{insert}\\ e\\ X) \\le M.eRk X$, then $\\operatorname{closure}(X) = \\operatorname{closure}(Y)$.$$

Lean4

theorem closure_eq_closure_of_subset_of_forall_insert (hX : M.IsRkFinite X) (hXY : X ⊆ Y)
    (hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X) : M.closure X = M.closure Y :=
  by
  refine hX.closure_eq_closure_of_subset_of_eRk_ge_eRk hXY <| not_lt.1 fun hlt ↦ ?_
  obtain ⟨z, hz, hr⟩ := exists_eRk_insert_eq_add_one_of_lt hlt
  simpa [hr, ENat.add_one_le_iff hX.eRk_lt_top.ne] using hY z hz

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