FormalConjecturesForMathlib/Order/Interval/Finset/Basic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. theorem Finset.Iio_eventually_nonempty line 24 source

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

    Statement uses: PartialOrder, LocallyFiniteOrder, OrderBot, Nontrivial, Exists, GE.ge, Finset.Nonempty, Finset.Iio

    Proof uses: Ne, Bot.bot, exists_ne, Exists.intro, of_eq_true, Eq.trans, Not, IsMin, True, False, congrArg, Eq, eq_false, ne_bot_of_le_ne_bot, not_false_eq_true

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. theorem Finset.Iio_eventually_card_ne_zero line 29 source

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

    Statement uses: PartialOrder, LocallyFiniteOrder, OrderBot, Nontrivial, Exists, GE.ge, Ne, Nat, Finset.card, Finset.Iio, OfNat.ofNat

    Proof uses: Finset.Nonempty, Finset.Iio_eventually_nonempty, Exists.intro, of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, Finset, EmptyCollection.emptyCollection, eq_false, Iff.mp, Finset.nonempty_iff_ne_empty, not_false_eq_true

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem Set.Iio_eventually_ncard_ne_zero line 35 source

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

    Statement uses: PartialOrder, LocallyFiniteOrder, OrderBot, Nontrivial, Exists, GE.ge, Ne, Nat, Set.ncard, Set.Iio, OfNat.ofNat

    Proof uses: Finset.card, Finset.Iio, Finset.Iio_eventually_card_ne_zero, Exists.intro, Eq.mpr, Finset, id, Eq, congrArg, Set, Eq.symm, Finset.coe_Iio, Set.ncard_coe_finset

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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