eRk_eq_of_eRk_insert_le_forall — Mathlib

English

If X ⊆ Y and for all e ∈ Y \\ X we have eRk(insert e X) ≤ eRk X, then the rank of X equals the rank of Y: eRk X = eRk Y.

Русский

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

LaTeX

$$$X \\subseteq Y \\; \\wedge\\; (\\forall e \\in Y \\setminus X,\\; M.eRk(\\mathrm{insert}\\ e\\ X) \\le M.eRk X) \\Rightarrow M.eRk X = M.eRk Y$$$

Lean4

theorem eRk_eq_of_eRk_insert_le_forall (hXY : X ⊆ Y) (hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X) :
    M.eRk X = M.eRk Y := by
  by_cases hX : M.IsRkFinite X
  · rw [← eRk_closure_eq, hX.closure_eq_closure_of_subset_of_forall_insert hXY hY, eRk_closure_eq]
  rw [eRk_eq_top_iff.2 hX, eRk_eq_top_iff.2 (mt (fun h ↦ h.subset hXY) hX)]

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