contract_contract_eq_contract_diff

English

Contracting first by C1 and then by C2 is the same as contracting by C1 and then by C2 \\ C1: M / C1 / C2 = M / C1 / (C2 \\ C1).

Русский

Сокращение сначала по C1, затем по C2 эквивалентно сокращению по C1, затем по C2 \\ C1: M / C1 / C2 = M / C1 / (C2 \\ C1).

LaTeX

$$$ (M / C_{1}) / C_{2} = M / C_{1} / (C_{2} \\ C_{1}) $$$

Lean4

theorem contract_contract_eq_contract_diff (M : Matroid α) (C₁ C₂ : Set α) : M ／ C₁ ／ C₂ = M ／ C₁ ／ (C₂ \ C₁) := by simp

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