Compare commits
2 Commits
main
...
fin-dom-ra
Author | SHA1 | Date |
---|---|---|
Joshua Potter | 870a01c6eb | |
Joshua Potter | a371cbb6f4 |
|
@ -935,23 +935,76 @@ natural numbers `m, n ∈ ω` such that `dom f ≈ m`, `ran f ≈ n`, and `m ≥
|
|||
theorem finite_dom_ran_size [Nonempty α] {A B : Set α}
|
||||
(hA : Set.Finite A) (hB : Set.Finite B) (hf : Set.MapsTo f A B)
|
||||
: ∃ m n : ℕ, A ≈ Set.Iio m ∧ f '' A ≈ Set.Iio n ∧ m ≥ n := by
|
||||
/-
|
||||
> Let `A` and `B` be finite sets and `f : A → B` be a function. By definition of
|
||||
> finite sets, there exists natural numbers `m, p ∈ ω` such that `A ≈ m` and
|
||||
> `B ≈ p`. By definition of the domain of a function, `dom f = A`. Thus
|
||||
> `dom f ≈ m`.
|
||||
-/
|
||||
have ⟨m, hm⟩ := Set.finite_iff_equinumerous_nat.mp hA
|
||||
have ⟨p, hp⟩ := Set.finite_iff_equinumerous_nat.mp hB
|
||||
/-
|
||||
> By *Theorem 6A*, there exists a one-to-one correspondence `g` between `m` and
|
||||
> `dom f = A`.
|
||||
-/
|
||||
have ⟨g, hg⟩ := Set.equinumerous_symm hm
|
||||
|
||||
/-
|
||||
> For all `y ∈ ran f`, consider `f⁻¹⟦{y}⟧`. Let
|
||||
>
|
||||
> `A_y = {x ∈ m | f(g(x)) = y}`.
|
||||
-/
|
||||
let A_y y := { x ∈ Set.Iio m | f (g x) = y }
|
||||
have hA₁ : ∀ y ∈ B, A_y y ≈ f ⁻¹' {y} := by
|
||||
/-
|
||||
> Since `g` is a one-to-one correspondence, it follows that `A_y ≈ f⁻¹⟦{y}⟧`.
|
||||
-/
|
||||
have hA₁ : ∀ y, y ∈ f '' A → A_y y ≈ A ∩ f ⁻¹' {y} := by
|
||||
intro y hy
|
||||
refine ⟨fun x => g x, ?_, ?_, ?_⟩
|
||||
· -- `Set.MapsTo`
|
||||
intro x hx
|
||||
simp only [Set.mem_Iio, Set.mem_setOf_eq, Set.mem_preimage, Set.mem_singleton_iff] at hx ⊢
|
||||
exact ⟨hg.left hx.left, hx.right⟩
|
||||
· -- `Set.InjOn`
|
||||
intro x₁ hx₁ x₂ hx₂ hf
|
||||
exact hg.right.left hx₁.left hx₂.left hf
|
||||
· -- `Set.SurjOn`
|
||||
unfold Set.SurjOn Set.preimage Set.image
|
||||
rw [Set.subset_def]
|
||||
simp only [Set.mem_singleton_iff, Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_Iio]
|
||||
intro x ⟨hx₁, hx₂⟩
|
||||
have hx₃ := hg.right.right hx₁
|
||||
simp only [Set.mem_image, Set.mem_Iio] at hx₃
|
||||
have ⟨z, hz⟩ := hx₃
|
||||
exact ⟨z, ⟨hz.left, hz.right ▸ hx₂⟩, hz.right⟩
|
||||
/-
|
||||
> Since `A_y` is a nonempty subset of natural numbers, the
|
||||
> *Well Ordering of `ω`* implies there exists a least element, say `q_y`.
|
||||
-/
|
||||
have hA₂ : ∀ y, y ∈ f '' A → Set.Nonempty (A_y y) := by
|
||||
intro y hy
|
||||
unfold Set.Nonempty
|
||||
simp only [Set.mem_image, Set.mem_Iio, Set.mem_setOf_eq] at hy ⊢
|
||||
have ⟨x, hx⟩ := hy
|
||||
have ⟨z, hz⟩ := hg.right.right hx.left
|
||||
simp only [Set.mem_Iio] at hz
|
||||
exact ⟨z, hz.left, hz.right ▸ hx.right⟩
|
||||
have hA₃ : ∀ y, y ∈ f '' A → ∃ q, q ∈ A_y y ∧ ∀ p ∈ A_y y, q ≤ p := by
|
||||
sorry
|
||||
have hA₂ : ∀ y ∈ B, Set.Nonempty (A_y y) := by
|
||||
sorry
|
||||
have hA₃ : ∀ y ∈ B, ∃ q : ℕ, ∀ p ∈ A_y y, q ≤ p := by
|
||||
sorry
|
||||
|
||||
let C := { q | ∃ y ∈ B, ∀ p ∈ A_y y, q ≤ p }
|
||||
/-
|
||||
> Define `C = {q_y | y ∈ ran f}`.
|
||||
-/
|
||||
let C := { q | ∃ y, y ∈ f '' A ∧ (∀ p ∈ A_y y, q ≤ p) }
|
||||
/-
|
||||
> Thus `h : C → ran f` given by `h(x) = f(g(x))` is a one-to-on ecorrespondence
|
||||
> between `C` and `ran f` by construction. That is, `C ≈ ran f`.
|
||||
-/
|
||||
let h x := f (g x)
|
||||
have hh : C ≈ f '' A := by
|
||||
sorry
|
||||
|
||||
/-
|
||||
> By *Lemma 6F*, there exists some `n ≤ m` such that `C ≈ n`. By *Theorem 6A*,
|
||||
> `n ≈ ran f`.
|
||||
-/
|
||||
sorry
|
||||
|
||||
/-- ### Set Difference Size
|
||||
|
|
Loading…
Reference in New Issue