Structures · Logic and sets
IsEmpty
IsEmpty α expresses that α is empty.
- Defined in
- Mathlib.Logic.IsEmpty.Defs
- Shape
- One type argument · adds false
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every IsEmpty is also a
Concrete types that are instances45
- Quiver.Hom
- TopCat.carrier
- NonemptyInterval
- CategoryTheory.Discrete
- SymAlg
- TopologicalSpace.NonemptyCompacts
- CategoryTheory.PreZeroHypercover.I₀
- Empty
- FundamentalGroupoid
- PEmpty
- PrimeSpectrum
- Ordinal.ToType
- Sym2
- PrincipalSeg
- LieModule.Weight
- SingularManifold.M
- Sym
- PProd
- Projectivization
- RelSeries
- SimpleGraph.ConnectedComponent
- False
- Function.Embedding
- PSum
- WType
- Multiset.ToType
- FirstOrder.Language.Relations
- FirstOrder.Language.Symbols
- SuccOrder
- PredOrder
- PSet.Type
- FirstOrder.Language.Functions
- SimpleGraph.Hom
- Subtype
- Prod
- Set.Elem
- ULift
- MulOpposite
- Fin
- AddOpposite
- Sum
- Sigma
- Quotient
- PLift
- Quot
How is a type an instance?
Loading the hierarchy index…
Assumed by442
- Set.iUnion_of_empty
- isEmptyElim
- Finset.univ_eq_empty
- IsEmpty.forall_iff
- Cardinal.mk_eq_zero
- IsEmpty.false
- ciSup_of_empty
- Set.iInter_of_empty
- Fintype.card_eq_zero
- Set.eq_empty_of_isEmpty
- iSup_of_empty'
- Function.isEmpty
- Real.iSup_of_isEmpty
- Set.range_eq_empty
- AlternatingMap.constOfIsEmpty
- iInf_of_empty
- iInf_of_isEmpty
- AlternatingMap.constLinearEquivOfIsEmpty
- linearIndependent_empty_type
- ContinuousAlternatingMap.constOfIsEmpty
- AlternatingMap.constLinearEquivOfIsEmpty_apply
- Matrix.det_isEmpty
- MvPolynomial.isEmptyRingEquiv
- Equiv.sumEmpty
- AlternatingMap.constOfIsEmpty_apply
- Filter.filter_eq_bot_of_isEmpty
- MeasureTheory.Measure.eq_zero_of_isEmpty
- IsEmpty.exists_iff
- tsum_empty
- MeasureTheory.Measure.pi_of_empty
- Matrix.trace_eq_zero_of_isEmpty
- Nat.card_of_isEmpty
- ContinuousMultilinearMap.constOfIsEmpty
- Orientation.eq_or_eq_neg_of_isEmpty
- Module.Basis.empty
- MvPolynomial.isEmptyAlgEquiv
- Finset.eq_empty_of_isEmpty
- OrderEmbedding.ofIsEmpty
- Matrix.coe_det_isEmpty
- Matrix.dotProduct_of_isEmpty
- iSup_of_empty
- FirstOrder.Language.LEquiv.addEmptyConstants
- Order.krullDim_eq_bot
- ContinuousAlternatingMap.constOfIsEmptyLIE
- MeasureTheory.lintegral_of_isEmpty
- Equiv.isEmpty
- ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty
- tprod_empty
- Module.Basis.det_isEmpty
- MultilinearMap.constOfIsEmpty
Ancestors59
- AlgebraicGeometry.IsAffine
- AlgebraicGeometry.IsAffineHom
- AlgebraicGeometry.IsClosedImmersion
- AlgebraicGeometry.IsFinite
- AlgebraicGeometry.IsImmersion
- AlgebraicGeometry.IsIntegralHom
- AlgebraicGeometry.IsLocallyArtinian
- AlgebraicGeometry.IsLocallyNoetherian
- AlgebraicGeometry.IsPreimmersion
- AlgebraicGeometry.IsProper
- AlgebraicGeometry.IsSeparated
- AlgebraicGeometry.LocallyOfFiniteType
- AlgebraicGeometry.LocallyQuasiFinite
- AlgebraicGeometry.QuasiCompact
- AlgebraicGeometry.QuasiCompactCover
- AlgebraicGeometry.QuasiSeparated
- AlgebraicGeometry.Scheme.IsQuasiAffine
- AlgebraicGeometry.Scheme.IsSeparated
- AlgebraicGeometry.SurjectiveOnStalks
- AlgebraicGeometry.UniversallyClosed
- CategoryTheory.CountableCategory
- CategoryTheory.FinCategory
- CompactSpace
- Countable
- Decidable
- Encodable
- Filter.TendstoCofinite
- Finite
- Fintype
- Inhabited
- IsOrderConnected
- IsStrictOrder
- IsStrictTotalOrder
- IsTrans
- IsWellFounded
- IsWellOrder
- Matroid.Finitary
- Matroid.Finite
- Matroid.InvariantCardinalRank
- Matroid.RankFinite
- MeasureTheory.IsFiniteMeasure
- MeasureTheory.SFinite
- MeasureTheory.SigmaFinite
- MeasureTheory.SignedMeasure.HaveLebesgueDecomposition
- Nonempty
- ProbabilityTheory.IsFiniteKernel
- ProbabilityTheory.IsMarkovKernel
- ProbabilityTheory.IsSFiniteKernel
- ProbabilityTheory.IsZeroOrMarkovKernel
- Small
- Std.Antisymm
- Std.Asymm
- Std.Irrefl
- Std.Trichotomous
- Subsingleton
- SummationFilter.HasSupport
- SummationFilter.LeAtTop
- Trans
- Unique