`BookProof.IrreversibleDynamics.exists_injective_not_surjective` {α : Type*} [Infinite α] : ∃ f : α → α, Function.Injective f ∧ ¬ Function.Surjective f

Initializing...

`BookProof.IrreversibleDynamics.exists_injective_not_surjective` {α : Type*} [Infinite α] : ∃ f : α → α, Function.Injective f ∧ ¬ Function.Surjective f · Prove2Me