exists_union_disjoint_cardinal_eq_of_infinite

English

If s is infinite, there exist two disjoint subsets t and u with t ∪ u = s and |t| = |u|.

Русский

Если s бесконечно, существуют два непересекающихся подмножества t и u такие, что t ∪ u = s и |t| = |u|.

LaTeX

$$$\\exists t,u:\\ t \\cup u = s \\land Disjoint(t,u) \\land \\#t = \\#u$$$

Lean4

theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) :
    ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u :=
  by
  have := h.to_subtype
  obtain ⟨f⟩ : Nonempty (s ≃ s ⊕ s) := by rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
  refine ⟨Subtype.val '' (f ⁻¹' (range .inl)), Subtype.val '' (f ⁻¹' (range .inr)), ?_, ?_, ?_⟩
  · simp [← image_union, ← preimage_union]
  · exact disjoint_image_of_injective Subtype.val_injective (isCompl_range_inl_range_inr.disjoint.preimage f)
  · simp [mk_image_eq Subtype.val_injective]

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