contract_eq_contract_iff — Mathlib

English

Two contractions M.contract C1 and M.contract C2 are equal if and only if their intersections with the ground are equal: M.contract C1 = M.contract C2 ⇔ C1 ∩ E = C2 ∩ E.

Русский

Два сокращения M.contract C1 и M.contract C2 равны тогда и только тогда, когда их пересечения с грунтом равны: M.contract C1 = M.contract C2 ⇔ C1 ∩ E = C2 ∩ E.

LaTeX

$$$ M.contract C_{1} = M.contract C_{2} \\iff C_{1} \\cap E = C_{2} \\cap E $$$

Lean4

theorem contract_eq_contract_iff : M ／ C₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E := by
  rw [← dual_delete_dual, ← dual_delete_dual, dual_inj, delete_eq_delete_iff, dual_ground]

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