|
|
import Mathlib
|
|
|
|
|
|
open Function Set
|
|
|
|
|
|
example {A B : Type _ } (f : A → B) : f.Injective ↔ ∃ g : B → A, g ∘ f = id := by
|
|
|
constructor
|
|
|
· intro h
|
|
|
-- hard.
|
|
|
sorry
|
|
|
· intro h
|
|
|
rcases h with ⟨g, h⟩
|
|
|
unfold Injective
|
|
|
intro a b hab
|
|
|
rw [←id_eq a, ←id_eq b]
|
|
|
rw [← h]
|
|
|
rw [comp_apply]
|
|
|
rw [hab]
|
|
|
simp
|
|
|
|
|
|
|
|
|
lemma singleton_mem_powerset
|
|
|
{U : Type _} {M : Set U} {x : U} (h : x ∈ M) :
|
|
|
{x} ∈ 𝒫 M := by
|
|
|
rw [mem_powerset_iff, singleton_subset_iff]
|
|
|
assumption
|
|
|
|
|
|
example
|
|
|
{U : Type _} (M : Set U) :
|
|
|
{A : Set U // A ∈ 𝒫 M} = {A ∈ 𝒫 M | True} := by
|
|
|
simp_rw [coe_setOf, and_true]
|
|
|
|
|
|
example
|
|
|
{U : Type _} (M : Set U) :
|
|
|
{A : Set U // A ∈ 𝒫 M} = 𝒫 M := by
|
|
|
rfl
|
|
|
|
|
|
example
|
|
|
{U : Type _} (M : Set U) :
|
|
|
{x : U // x ∈ M} = M := by
|
|
|
rfl
|
|
|
|
|
|
example
|
|
|
{U : Type _} (M : Set U) :
|
|
|
∃ (f : M → 𝒫 M), Injective f := by
|
|
|
use fun x ↦ ⟨ _, singleton_mem_powerset x.prop ⟩
|
|
|
intro a b hab
|
|
|
simp at hab
|
|
|
rw [Subtype.val_inj] at hab
|
|
|
assumption
|
|
|
|
|
|
instance {U : Type _} {M : Set U} : Membership ↑M ↑(𝒫 M) :=
|
|
|
{ mem := fun x A ↦ x.1 ∈ A.1 }
|
|
|
|
|
|
instance {U : Type _} {M : Set U} : Membership U (Set ↑M) :=
|
|
|
{ mem := fun x A ↦ _ }
|
|
|
|
|
|
|
|
|
example
|
|
|
{U : Type _} {M : Set U} (h_empty : M.Nonempty)
|
|
|
(f : {x : U // x ∈ M} → {A : Set U // A ∈ 𝒫 M}):
|
|
|
¬ Surjective f := by
|
|
|
unfold Surjective
|
|
|
push_neg
|
|
|
--by_contra h_sur
|
|
|
let B : Set M := {x : M | x ∉ (f x)}
|
|
|
use ⟨B, sorry⟩
|
|
|
intro ⟨a, ha⟩
|
|
|
sorry
|
|
|
-- Too hard?
|
|
|
|
|
|
#check singleton_mem_powerset
|
|
|
#check Subtype.val_inj
|
|
|
|
|
|
|
|
|
|
|
|
-- These are fun exercises for prime.
|
|
|
example (x : ℕ) : 0 < x ↔ 1 ≤ x := by
|
|
|
rfl
|
|
|
|
|
|
lemma le_cancel_left (n x : ℕ) (h : x ≠ 0): n ≤ n * x := by
|
|
|
induction n
|
|
|
simp
|
|
|
simp
|
|
|
rw [← zero_lt_iff] at h
|
|
|
assumption
|
|
|
|
|
|
|
|
|
example (n m : ℕ) (g : m ≠ 0) (h : n ∣ m) : n ≤ m := by
|
|
|
rcases h with ⟨x, hx⟩
|
|
|
rw [hx]
|
|
|
apply le_cancel_left
|
|
|
by_contra k
|
|
|
rw [k] at hx
|
|
|
simp at hx
|
|
|
rw [hx] at g
|
|
|
contradiction
|