English
A generalization of Marica–Schonheim inequality for finite set systems: the product of two subset-cardinalities is bounded by a product of the cardinalities of the respective symmetric differences of the two families.
Русский
Обобщение неравенства Марича–Шёнхайма для конечных семейств множеств: произведение кардинальностей двух подсемейств ограничено произведением кардинальностей соответствующих симметрических различий двух семейств.
LaTeX
$$$$|s|\\cdot|t| \\le |s\\setminus t|\\cdot|t\\setminus s|$$$$
Lean4
/-- A slight generalisation of the **Marica-Schönheim Inequality**. -/
theorem le_card_diffs_mul_card_diffs (s t : Finset α) : #s * #t ≤ #(s \\ t) * #(t \\ s) :=
by
have :
∀ s t : Finset α,
(s \\ t).map ⟨_, liftLatticeHom_injective⟩ =
s.map ⟨_, liftLatticeHom_injective⟩ \\ t.map ⟨_, liftLatticeHom_injective⟩ :=
by
rintro s t
simp_rw [map_eq_image]
exact image_image₂_distrib fun a b ↦ rfl
simpa [← card_compls (_ ⊻ _), ← map_sup, ← map_inf, ← this] using
(s.map ⟨_, liftLatticeHom_injective⟩).le_card_infs_mul_card_sups (t.map ⟨_, liftLatticeHom_injective⟩)ᶜˢ
