exists_union_disjoint_cardinal_eq_iff

English

Even (s.ncard) holds if and only if there exist t,u with t ∪ u = s, Disjoint t u, and |t| = |u|.

Русский

Чётная мощность s эквивалентна существованию разбиения на два непересекающихся подмножества с равной мощностью.

LaTeX

$$$\\text{Even}(s.ncard) \\iff \\exists t,u:\\ t \\cup u = s \\land Disjoint(t,u) \\land |t| = |u|$$$

Lean4

theorem exists_union_disjoint_cardinal_eq_iff (s : Set α) :
    Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u :=
  by
  use exists_union_disjoint_cardinal_eq_of_even
  rintro ⟨t, u, rfl, hdtu, hctu⟩
  obtain hfin | hnfin := (t ∪ u).finite_or_infinite
  · rw [finite_union] at hfin
    have hn : t.ncard = u.ncard := congrArg Cardinal.toNat hctu
    rw [ncard_union_eq hdtu hfin.1 hfin.2, hn]
    exact Even.add_self u.ncard
  · simp [hnfin.ncard]

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