dens_sdiff_comm — Mathlib

English

If card(s) = card(t), then dens(s \\ t) = dens(t \\ s).

Русский

Если карточка подмножеств равна, то плотности разностей равны: dens(s \\ t) = dens(t \\ s).

LaTeX

$$$ \\operatorname{dens}(s \\ t) = \\operatorname{dens}(t \\ s) \\quad \\text{если } |s| = |t| $$$

Lean4

theorem dens_sdiff_comm (h : card s = card t) : dens (s \ t) = dens (t \ s) :=
  add_left_injective (dens t) <| by simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]

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