English
Any two distinct blocks in memPartition(f,n) are disjoint.
Русский
Любые две разные части в memPartition(f,n) попарно не пересекаются.
LaTeX
$$$\\forall u,v \\in \\operatorname{memPartition}(f,n),\ u \\neq v \\Rightarrow u \\cap v = \\emptyset$$$
Lean4
theorem disjoint_memPartition (f : ℕ → Set α) (n : ℕ) {u v : Set α} (hu : u ∈ memPartition f n)
(hv : v ∈ memPartition f n) (huv : u ≠ v) : Disjoint u v :=
by
revert u v
induction n with
| zero =>
intro u v hu hv huv
simp only [memPartition_zero, mem_singleton_iff] at hu hv
rw [hu, hv] at huv
exact absurd rfl huv
| succ n ih =>
intro u v hu hv huv
rw [memPartition_succ] at hu hv
obtain ⟨u', hu', hu'_eq⟩ := hu
obtain ⟨v', hv', hv'_eq⟩ := hv
rcases hu'_eq with rfl | rfl <;> rcases hv'_eq with rfl | rfl
· refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)
exact fun huv' ↦ huv (huv' ▸ rfl)
· exact Disjoint.mono_left inter_subset_right Set.disjoint_sdiff_right
· exact Disjoint.mono_right inter_subset_right Set.disjoint_sdiff_left
· refine Disjoint.mono diff_subset diff_subset (ih hu' hv' ?_)
exact fun huv' ↦ huv (huv' ▸ rfl)
