Lumenary.Functions

Formal library

• BijectivedefDefinitionNo axioms

  /-- A function is **bijective** when it is both injective and surjective: every element of
  the target is hit by exactly one input. -/
  def Bijective (f : α → β) : Prop := Injective f ∧ Surjective f

  Axioms used: No axiomsformal/Lumenary/Functions.leanTry it in the Lean web editor

• injective_two_mul_add_onetheoremProved here from basic factspropext

  /-- `n ↦ 2n + 1` is injective: if `2a + 1 = 2b + 1`, subtract 1 and divide by 2. -/
  theorem injective_two_mul_add_one : Injective (fun n : Int => 2 * n + 1) := by
    intro a b h
    -- `h : 2 * a + 1 = 2 * b + 1`
    have h1 : 2 * a = 2 * b := (Int.add_left_inj 1).mp h      -- subtract 1
    exact Int.eq_of_mul_eq_mul_left (by decide) h1           -- divide by 2 (and 2 ≠ 0)

  Axioms used: propextformal/Lumenary/Functions.leanTry it in the Lean web editor

• not_injective_squaretheoremProved here from basic factsNo axioms

  /-- `n ↦ n²` is **not** injective on the integers: `1² = (-1)²` but `1 ≠ -1`. -/
  theorem not_injective_square : ¬ Injective (fun n : Int => n * n) := by
    intro h
    have h1 : (1 : Int) = -1 := h (by decide)   -- the hypothesis needed is `1 * 1 = -1 * -1`
    exact absurd h1 (by decide)

  Axioms used: No axiomsformal/Lumenary/Functions.leanTry it in the Lean web editor

• surjective_add_onetheoremProved here from basic factspropext

  /-- `n ↦ n + 1` is surjective on the integers: to hit `y`, start from `y - 1`. -/
  theorem surjective_add_one : Surjective (fun n : Int => n + 1) := by
    intro y
    exact ⟨y - 1, Int.sub_add_cancel y 1⟩

  Axioms used: propextformal/Lumenary/Functions.leanTry it in the Lean web editor

• not_surjective_two_multheoremProved here from basic factspropext

  /-- `n ↦ 2n` is **not** surjective on the integers: nothing is sent to `1`, because there is
  no integer half (`Lumenary.Integers.no_int_half`). -/
  theorem not_surjective_two_mul : ¬ Surjective (fun n : Int => 2 * n) := by
    intro h
    obtain ⟨x, hx⟩ := h 1          -- `hx : 2 * x = 1`
    exact Lumenary.Integers.no_int_half ⟨x, hx⟩

  Axioms used: propextformal/Lumenary/Functions.leanTry it in the Lean web editor

• bijective_negtheoremProved here from basic factsNo axioms

  /-- Negation `n ↦ -n` is a bijection of the integers (it is its own inverse). -/
  theorem bijective_neg : Bijective (fun n : Int => -n) := by
    constructor
    · -- Injective: from `-a = -b`, negate both sides.
      intro a b h
      exact Int.neg_inj.mp h
    · -- Surjective: `-(-y) = y`.
      intro y
      exact ⟨-y, Int.neg_neg y⟩

  Axioms used: No axiomsformal/Lumenary/Functions.leanTry it in the Lean web editor

• graphdefDefinitionNo axioms

  /-- The **graph** of `f`: the set of pairs `(a, b)` with `f a = b`, written as a predicate on
  pairs (in `Lumenary.Sets` this is a `Set (α × β)`). In set theory a function *is* such a set
  of pairs. -/
  def graph (f : α → β) : α × β → Prop := fun p => f p.1 = p.2

  Axioms used: No axiomsformal/Lumenary/Functions.leanTry it in the Lean web editor

• graph_functionaltheoremProved here from basic factsNo axioms

  /-- A graph is **functional**: each input `a` is paired with `f a`, and with nothing else. -/
  theorem graph_functional (f : α → β) (a : α) :
      graph f (a, f a) ∧ ∀ b, graph f (a, b) → b = f a := by
    constructor
    · -- `graph f (a, f a)` says `f a = f a`.
      rfl
    · intro b h
      -- `h : f a = b`
      exact Eq.symm h

  Axioms used: No axiomsformal/Lumenary/Functions.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- A composite of injective functions is injective.
Hint: `intro a b h`; here `h : g (f a) = g (f b)`. Use `hg` first, then `hf`. -/
theorem injective_comp {f : α → β} {g : β → γ} (hg : Injective g) (hf : Injective f) :
    Injective (g ∘ f) := by
  sorry

/-- A composite of injective functions is injective.
If `g (f a) = g (f b)`, injectivity of `g` gives `f a = f b`, and then injectivity of `f`
gives `a = b`. (Core analogue: `Function.Injective.comp`.) -/
theorem injective_comp {f : α → β} {g : β → γ} (hg : Injective g) (hf : Injective f) :
    Injective (g ∘ f) := by
  intro a b h
  -- `h : g (f a) = g (f b)`
  have hfab : f a = f b := hg h
  exact hf hfab

/-- A composite of surjective functions is surjective.
Hint: `intro c`, then `obtain ⟨b, hb⟩ := hg c` and `obtain ⟨a, ha⟩ := hf b`. -/
theorem surjective_comp {f : α → β} {g : β → γ} (hg : Surjective g) (hf : Surjective f) :
    Surjective (g ∘ f) := by
  sorry

/-- A composite of surjective functions is surjective.
To hit `c`, first find `b` with `g b = c`, then `a` with `f a = b`; then `g (f a) = c`.
(Core analogue: `Function.Surjective.comp`.) -/
theorem surjective_comp {f : α → β} {g : β → γ} (hg : Surjective g) (hf : Surjective f) :
    Surjective (g ∘ f) := by
  intro c
  obtain ⟨b, hb⟩ := hg c      -- `hb : g b = c`
  obtain ⟨a, ha⟩ := hf b      -- `ha : f a = b`
  refine ⟨a, ?_⟩
  show g (f a) = c
  rw [ha, hb]