PFR/Mathlib/Data/Set/Card.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
Imported by 2 files
  1. lemma Set.ncard_singleton_inter' line 14 source

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

    Statement uses: Set, Decidable, Membership.mem, Eq, Nat, Set.ncard, Inter.inter, Singleton.singleton, ite, OfNat.ofNat

    Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, of_eq_true, Eq.trans, True, congrFun', Set.inter_eq_left', LE.le, eq_true, Set.ncard_singleton, eq_self, Not, ite_eq_right, EmptyCollection.emptyCollection, Set.singleton_inter_of_notMem, False, eq_false and 2 more

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. lemma Set.ncard_inter_singleton line 18 source

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

    Statement uses: Set, Decidable, Membership.mem, Eq, Nat, Set.ncard, Inter.inter, Singleton.singleton, ite, OfNat.ofNat

    Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, of_eq_true, Eq.trans, True, congrFun', Set.inter_eq_right', LE.le, eq_true, Set.ncard_singleton, eq_self, Not, ite_eq_right, EmptyCollection.emptyCollection, Set.inter_singleton_of_notMem, False, eq_false and 2 more

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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