FormalConjecturesForMathlib/SetTheory/Cardinal/Arithmetic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 1 file
  1. lemma Cardinal.aleph0_le_mk_set line 25 source

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

    Statement uses: Set, Iff, LE.le, Cardinal, Cardinal.aleph0, Cardinal.mk, Set.Infinite

    Proof uses: Eq.mpr, Infinite, id, Eq, congrArg, propext, Cardinal.aleph0_le_mk_iff, Set.infinite_coe_iff, Iff.rfl

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma Cardinal.mk_sdiff_eq_left' line 29 source

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

    Statement uses: Set, Set.Infinite, LT.lt, Cardinal, Cardinal.mk, Inter.inter, Eq, SDiff.sdiff

    Proof uses: LE.le.eq_of_not_lt, Cardinal.mk_le_mk_of_subset, Set.sdiff_subset, LT.lt.not_ge, HAdd.hAdd, Cardinal.add_lt_of_lt, Eq.mpr, LE.le, Cardinal.aleph0, id, le_imp_le_of_le_of_le, Union.union, le_refl, Cardinal.mk_union_le, congrArg, Set.inter_union_sdiff

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. lemma Cardinal.mk_sdiff_eq_left line 35 source

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

    Statement uses: Set, Set.Infinite, LT.lt, Cardinal, Cardinal.mk, Eq, SDiff.sdiff

    Proof uses: Cardinal.mk_sdiff_eq_left', LT.lt.trans_le', Inter.inter, Cardinal.mk_subtype_mono, Membership.mem, Set.inter_subset_right

    11 instances, coercions and auxiliary constants left out.

  4. lemma Cardinal.mk_sdiff_eq_left_of_finite' line 39 source

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

    Statement uses: Set, Set.Infinite, Set.Finite, Inter.inter, Eq, Cardinal, Cardinal.mk, SDiff.sdiff

    Proof uses: Cardinal.mk_sdiff_eq_left', LE.le.trans_lt', Cardinal.aleph0, Iff.mpr, LE.le, Cardinal.aleph0_le_mk_set, Eq.mpr, LT.lt, id, Eq.trans, Subtype, Membership.mem, Set.ofPred, congrArg, And, funext

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. lemma Cardinal.mk_sdiff_eq_left_of_finite line 43 source

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

    Statement uses: Set, Set.Infinite, Set.Finite, Eq, Cardinal, Cardinal.mk, SDiff.sdiff

    Proof uses: Cardinal.mk_sdiff_eq_left, LE.le.trans_lt', Cardinal.aleph0, Iff.mpr, LE.le, Cardinal.aleph0_le_mk_set, Eq.mpr, LT.lt, id, Membership.mem

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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