surjective_finite

Prove that Finite B knowing that Finite A and there exists a surjection f from A to B.

I think the premise says that A and B are bijective, so I am not sure how this differs from bijective_finite apart from the functions in the premise being swapped.

added 1 commit

• c7fb75a1 - prove bijective_finite from injective_finite

Compare with previous version

A and B don't have to be bijective, Cancel (=) g f is assumed, not Cancel (=) f g which would indeed imply bijectivity.

We can prove the following for instance.

  Inductive Foo: Type := Foo1.
  Inductive Bar: Type := Bar1 | Bar2.

  Instance Foo_eq_dec: EqDecision Foo. solve_decision. Qed.
  Instance Bar_eq_dec: EqDecision Bar. solve_decision. Qed.

  Instance Bar_finite: Finite Bar. Admitted.

  Instance Foo_finite: Finite Foo.
  eapply injective_finite with (f := fun _ => Bar1) (g := fun _ => Foo1).
  intro x. destruct x; reflexivity.
  Qed.

added 1 commit

• 57a1a207 - surjective_finite

Compare with previous version

changed title from injective_finite to surjective_finite

changed the description

After some thought, I realized that you only need to know a surjective function from a finite type to another to conclude about finiteness of the second type.

After some thought, I realized that you only need to know a surjective function from a finite type to another to conclude about finiteness of the second type.

Well caught. That's much nicer.

added 1 commit

• 57c98ce1 - Apply Robbert's suggestions

Compare with previous version

resolved all threads

merged

mentioned in commit f59a2c06

Merged and many thanks!