bagInter_left — Mathlib

English

If t1 ~ t2, then l.bagInter t1 = l.bagInter t2 for any l.

Русский

Если t1 перестановочно эквивалентен t2, то l.bagInter t1 = l.bagInter t2 для любого l.

LaTeX

$$$t_1 \\sim t_2 \\Rightarrow l.bagInter t_1 = l.bagInter t_2$$$

Lean4

theorem bagInter_left (l : List α) {t₁ t₂ : List α} (p : t₁ ~ t₂) : l.bagInter t₁ = l.bagInter t₂ :=
  by
  induction l generalizing t₁ t₂ p with
  | nil => simp
  | cons a l IH => ?_
  by_cases h : a ∈ t₁
  · simp [h, p.subset h, IH (p.erase _)]
  · simp [h, mt p.mem_iff.2 h, IH p]

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