PFR/Mathlib/Order/Interval/Finset/Defs.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Finset.Ici_one line 10 source

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

    Statement uses: One, Preorder, IsBotOneClass, LocallyFiniteOrderTop, Fintype, Eq, Finset, Finset.Ici, OfNat.ofNat, Finset.univ

    Proof uses: Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congr, congrArg, congrFun', Finset.Ici_one_eq_univ, iff_self

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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