Mathlib Map

Theorems · Theorem · order theory

Set.EqOn.trans

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ f₃ : α → β}, Set.EqOn f₁ f₂ s → Set.EqOn f₂ f₃ s → Set.EqOn f₁ f₃ s
Defined in
Mathlib.Data.Set.Function
Cited by
13 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Manifold.isLocalSourceTargetProperty_immersionAtProp · cited by 3Manifold.isLocalSourceTar…Manifold.isLocalSourceTargetProperty_submmersionAtProp · cited by 3Manifold.isLocalSourceTar…Complex.one_add_cpow_hasFPowerSeriesOnBall_zero · cited by 3Complex.one_add_cpow_hasF…Manifold.IsSubmersionAtOfComplement.trans_F · cited by 2IsSubmersionAtOfComplemen…Manifold.IsImmersionAtOfComplement.trans_F · cited by 2IsImmersionAtOfComplement…iteratedDerivWithin_of_isOpen_eq_iterate · cited by 2iteratedDerivWithin_of_is…hasProdUniformlyOn_of_clog · cited by 1hasProdUniformlyOn_of_clogeqOn_iteratedDerivWithin_cotTerm_integerComplement · cited by 1eqOn_iteratedDerivWithin_…eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet · cited by 1eqOn_iteratedDerivWithin_…OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source · cited by 1EqOn.restr_eqOn_sourceiteratedDerivWithin_zpow · cited by 0iteratedDerivWithin_zpowiteratedDerivWithin_one_div · cited by 0iteratedDerivWithin_one_d…logDeriv_eqOn_iff · cited by 0logDeriv_eqOn_iffSet · cited by 53352SetSet.EqOn · cited by 603Set.EqOnEqOn.transCITED BYCITES

Cites2

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

  • Setstatement and proof · cited by 53,352
  • Set.EqOnstatement and proof · cited by 603

Cited by13

Results whose statement or proof uses this declaration.