Mathlib Map

Theorems · Theorem · order theory

Sigma.subtype_ext

∀ {α : Type u_1} {β : Type u_7} {p : α → β → Prop} {x₀ x₁ : (a : α) × Subtype (p a)},
  x₀.fst = x₁.fst → ↑x₀.snd = ↑x₁.snd → x₀ = x₁

A specialized ext lemma for equality of sigma types over an indexed subtype.

Defined in
Mathlib.Data.Sigma.Basic
Cited by
8 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AddMonoidAlgebra.decomposeAux_single · cited by 3AddMonoidAlgebra.decompos…CliffordAlgebra.GradedAlgebra.ι_sq_scalar · cited by 1GradedAlgebra.ι_sq_scalarSym.sigma_sub_ext · cited by 1Sym.sigma_sub_extConfiguration.ProjectivePlane.card_points · cited by 1ProjectivePlane.card_poin…CliffordAlgebra.GradedAlgebra.lift_ι_eq · cited by 0GradedAlgebra.lift_ι_eqSigma.subtype_ext_iff · cited by 0Sigma.subtype_ext_iffExteriorAlgebra.GradedAlgebra.liftι_eq · cited by 0GradedAlgebra.liftι_eqTopologicalSpace.Fiber.sigmaIsoHom_inj · cited by 0Fiber.sigmaIsoHom_injSigma.subtype_extCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by8

Results whose statement or proof uses this declaration.