coindep_contract_of_disjoint — Mathlib

English

If X is coindependent in M and X is disjoint from C, then X is coindependent in M / C.

Русский

Если X коиндепендентно в M и X не пересекается с C, то X коиндепендентно и после сокращения M / C.

LaTeX

$$$ (M / C).Coindep X = (M.Coindep X) \text{ when }\ Disjoint(X, C) $$$

Lean4

theorem coindep_contract_of_disjoint (hX : M.Coindep X) (hXC : Disjoint X C) : (M ／ C).Coindep X :=
  coindep_contract_iff.2 ⟨hX, hXC⟩

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