pith. machine review for the scientific record. sign in
lemma proved tactic proof

no_surj_small

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  41lemma no_surj_small (T d : Nat) (hT : T < 2 ^ d) :
  42  ¬ ∃ f : Fin T → Pattern d, Function.Surjective f := by

proof body

Tactic-mode proof.

  43  classical
  44  intro h; rcases h with ⟨f, hf⟩
  45  obtain ⟨g, hg⟩ := hf.hasRightInverse
  46  have hginj : Injective g := by
  47    intro y₁ y₂ hgy
  48    have : f (g y₁) = f (g y₂) := by simp [hgy]
  49    simpa [RightInverse, hg y₁, hg y₂] using this
  50  have hcard : Fintype.card (Pattern d) ≤ Fintype.card (Fin T) :=
  51    Fintype.card_le_of_injective _ hginj
  52  have : 2 ^ d ≤ T := by
  53    simpa [Fintype.card_fin, card_pattern d] using hcard
  54  exact (lt_of_le_of_lt this hT).false
  55
  56/-- Minimal ticks lower bound for a complete cover. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.