Ideal

Statistics

Metric	Count
Definitions	0
Theorems `iSup_iInf_eq_top_iff_pairwise`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_iInf_eq_top_iff_pairwise` 📖	mathematical	`Finset.Nonempty`	`iSup` `Ideal` `CommSemiring.toSemiring` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Finset` `Finset.instMembership` `iInf` `Submodule.instInfSet` `Top.top` `Submodule.instTop` `Set.Pairwise` `SetLike.coe` `Finset.instSetLike` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id`	—	`eq_top_iff_one` `Submodule.mem_iSup_finset_iff_exists_sum` `Finset.Nonempty.cons_induction` `Finset.sum_singleton` `Finset.coe_singleton` `iInf_congr_Prop` `iInf_iInf_eq_left` `iInf_neg` `Finset.coe_cons` `Set.pairwise_insert_of_symmetric` `sup_comm` `Submodule.coe_mem` `mem_iInf` `Finset.subset_cons` `Finset.sum_cons` `Finset.sum_congr` `Pi.add_apply` `Submodule.coe_add` `Pi.single_eq_same` `Pi.single_eq_of_ne` `Submodule.coe_zero` `Finset.sum_add_distrib` `Finset.sum_pi_single'` `Submodule.mem_sup` `sum_mem` `Finset.mem_cons_self` `add_comm` `sup_iInf_eq_top` `instIsTwoSided` `Finset.mem_cons` `mul_mem_right` `mul_mem_left` `mul_one` `Finset.mul_sum`

---