FormalConjecturesForMathlib/Topology/Algebra/InfiniteSum/Order.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Multipliable.prod_le_tprod_set line 27 source

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

    Statement uses: PartialOrder, CommGroup, IsOrderedMonoid, UniformSpace, IsUniformGroup, CompleteSpace, OrderClosedTopology, Finset, Set, LE.le, Not, Membership.mem, OfNat.ofNat, Multipliable, SummationFilter.unconditional, Finset.prod, tprod

    Proof uses: Eq.mpr, Set.mulIndicator, id, Eq, congrArg, tprod_subtype, Finset.prod_congr, rfl, of_eq_true, Eq.trans, True, ite_cond_eq_true, Classical.decPred, eq_true, eq_self, Multipliable.prod_le_tprod, forall_congr, ite, implies_congr, Eq.refl and 3 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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