MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean

GitHub source file

7 declarations, 3 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. def sbAux line 15 source

    no axioms what this means

    Statement uses: Nat, Set

    2 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean:15 (same declaration text).

  2. def sbSet line 19 source

    no axioms what this means

    Statement uses: Set

    Proof uses: Set.iUnion, Nat, sbAux

    Also declared: MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean:19 (same declaration text).

  3. def sbFun line 22 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nonempty

    Proof uses: ite, Membership.mem, Set, sbSet, Function.invFun

    2 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean:22 (same declaration text).

  4. theorem sb_right_inv sorry line 25 source

    depends on sorry what this means

    Statement uses: Nonempty, Not, Membership.mem, Set, sbSet, Eq, Function.invFun

    Proof uses: Set.image, Set.univ, Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr, Set.iUnion, Nat, sbAux, id, congrArg, sbSet.eq_1, Exists, propext, Set.mem_iUnion, Exists.intro, OfNat.ofNat, SDiff.sdiff, sbAux.eq_1, And, Set.mem_diff, sorryAx and 5 more

    4 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean:25 (same statement text; different proof or body). Qualify references as sb_right_inv@path.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  5. theorem sb_injective sorry line 36 source

    depends on sorry what this means

    Statement uses: Nonempty, Function.Injective, sbFun

    Proof uses: Set, sbSet, Eq, rfl, Eq.mpr, id, congrArg, dite, Or, Membership.mem, Not, Classical.em, ite, Function.invFun, Iff.mp, not_imp_self, sorryAx, Lean.Name, Bool.false, Lean.Name.num and 25 more

    10 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean:37 (same statement text; different proof or body). Qualify references as sb_injective@path.

    Tactic trace: 26 steps

    Open to load the checked before-and-after goal states.

  6. theorem sb_surjective sorry line 62 source

    depends on sorry what this means

    Statement uses: Nonempty, Function.Injective, Function.Surjective, sbFun

    Proof uses: Set, sbSet, Eq, rfl, Eq.mpr, id, congrArg, dite, Exists, Membership.mem, Nat, sbAux, Eq.mp, Set.iUnion, propext, Set.mem_iUnion, sbSet.eq_1, Nat.casesAuxOn, OfNat.ofNat, False.elim and 27 more

    14 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean:65 (same statement text; different proof or body). Qualify references as sb_surjective@path.

    Tactic trace: 19 steps

    Open to load the checked before-and-after goal states.

  7. theorem schroeder_bernstein line 84 source

    depends on sorry what this means

    Statement uses: Nonempty, Function.Injective, Exists, Function.Bijective

    Proof uses: Exists.intro, sbFun, And.intro, Function.Surjective, sb_injective, sb_surjective