isPartition_iff_iUnion_eq — Mathlib

English

Another simp-variant: π.IsPartition ↔ π.iUnion = I.toSet (alternative form).

Русский

Ещё одна упрощённая версия: π.IsPartition ↔ π.iUnion = I.toSet (альтернативная форма).

LaTeX

$$$ π.IsPartition \iff π.iUnion = I.toSet. $$$

Lean4

theorem isPartition_iff_iUnion_eq {π : Prepartition I} : π.IsPartition ↔ π.iUnion = I := by
  simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def, mem_iUnion, Box.mem_coe]

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