Theorems · Theorem · order theory
Equiv.iSup_comp
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : SupSet α] {g : ι' → α} (e : ι ≃ ι'), ⨆ x, g (e x) = ⨆ y, g y- Defined in
- Mathlib.Order.CompleteLattice.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
- Assumes
- SupSet
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement and proof · cited by 8,337
- iSupstatement · cited by 2,415
- Equiv.surjectiveproof · cited by 198
- SupSetstatement and proof · cited by 154
- Function.Surjective.iSup_compproof · cited by 9
Cited by14
Results whose statement or proof uses this declaration.
- LieModule.iSup_genWeightSpace_eq_top'proof · cited by 5
- iInf_iSup_eq_of_finiteproof · cited by 2
- Ordinal.mem_closure_tfaeproof · cited by 1
- Set.Finite.biInf_iSup_eqproof · cited by 1
- Subspace.dualAnnihilator_iInf_eqproof · cited by 1
- LieAlgebra.Basis.borelUpper_le_biSupproof · cited by 1
- Order.Ideal.iSup_mem_iffproof · cited by 1
- MeasureTheory.addContent_le_sum_of_subset_sUnionproof · cited by 1
- Ordinal.rank_toPSetproof · cited by 1
- AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isComplproof · cited by 1
- Equiv.biSup_compproof · cited by 1
- Ordinal.card_iSup_Iio_le_sum_cardproof · cited by 1