diff_subset_loops_contract — Mathlib

English

If I X is a basis, then X \\ I is contained in the loops of M / I.

Русский

Если I X образуют базис, то X \\ I состоит только из петель после сокращения по I.

LaTeX

$$$(M.IsBasis I X) \\Rightarrow (X \\setminus I) \\subseteq (M / I).loops$$

Lean4

theorem diff_subset_loops_contract (hIX : M.IsBasis I X) : X \ I ⊆ (M ／ I).loops :=
  by
  rw [diff_subset_iff, contract_loops_eq, union_diff_self, union_eq_self_of_subset_left (M.subset_closure I)]
  exact hIX.subset_closure

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