Sign

📁 Source: Mathlib/Topology/Instances/Sign.lean

Statistics

Metric	Count
Definitions Sign, instTopologicalSpaceSignType	2
Theorems continuousAt_sign_of_ne_zero, continuousAt_sign_of_neg, continuousAt_sign_of_pos, instDiscreteTopologySignType	4
Total	6

Mathlib.Tactic.FieldSimp

Definitions

Name	Category	Theorems
Sign 📖	CompData	—

(root)

Definitions

Name	Category	Theorems
instTopologicalSpaceSignType 📖	CompOp	6 math math: Real.Angle.continuousAt_sign, ContinuousOn.angle_sign_comp, instDiscreteTopologySignType, continuousAt_sign_of_neg, continuousAt_sign_of_pos, continuousAt_sign_of_ne_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_sign_of_ne_zero 📖	mathematical	—	ContinuousAt SignType instTopologicalSpaceSignType DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign LinearOrder.toDecidableLT	—	Ne.lt_or_gt continuousAt_sign_of_neg continuousAt_sign_of_pos
continuousAt_sign_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	ContinuousAt SignType instTopologicalSpaceSignType DFunLike.coe OrderHom SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign	—	ContinuousAt.congr continuousAt_const Filter.EventuallyEq.eq_1 eventually_nhds_iff sign_neg isOpen_gt'
continuousAt_sign_of_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	ContinuousAt SignType instTopologicalSpaceSignType DFunLike.coe OrderHom SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign	—	ContinuousAt.congr continuousAt_const Filter.EventuallyEq.eq_1 eventually_nhds_iff sign_pos isOpen_lt'
instDiscreteTopologySignType 📖	mathematical	—	DiscreteTopology SignType instTopologicalSpaceSignType	—	—

---

← Back to Index