HarmonicContOnCl

📁 Source: Mathlib/Analysis/InnerProductSpace/Harmonic/HarmonicContOnCl.lean

Statistics

Metric	Count
Definitions HarmonicContOnCl	1
Theorems add, add_const, const_add, const_smul, const_sub, contDiffAt, continuousOn, continuousOn_ball, differentiableAt, fun_add, fun_add_const, fun_const_add, fun_const_smul, fun_const_sub, fun_neg, fun_sub, fun_sub_const, harmonicOnNhd, mk_ball, mono, neg, sub, sub_const, harmonicContOnCl, harmonicContOnCl_iff, harmonicContOnCl_const	26
Total	27

InnerProductSpace

Definitions

Name	Category	Theorems
HarmonicContOnCl 📖	CompData	21 math math: HarmonicContOnCl.sub_const, HarmonicContOnCl.add, HarmonicContOnCl.const_sub, HarmonicContOnCl.fun_sub, HarmonicContOnCl.neg, HarmonicContOnCl.fun_sub_const, HarmonicOnNhd.harmonicContOnCl, harmonicContOnCl_const, HarmonicContOnCl.const_smul, HarmonicContOnCl.mk_ball, HarmonicContOnCl.fun_const_add, HarmonicContOnCl.const_add, HarmonicContOnCl.fun_add_const, HarmonicContOnCl.sub, HarmonicContOnCl.fun_const_smul, HarmonicContOnCl.mono, HarmonicContOnCl.add_const, HarmonicContOnCl.fun_const_sub, IsClosed.harmonicContOnCl_iff, HarmonicContOnCl.fun_neg, HarmonicContOnCl.fun_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonicContOnCl_const 📖	mathematical	—	HarmonicContOnCl	—	harmonicOnNhd_const continuousOn_const

InnerProductSpace.HarmonicContOnCl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	InnerProductSpace.HarmonicOnNhd.add harmonicOnNhd ContinuousOn.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup continuousOn
add_const 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add InnerProductSpace.harmonicContOnCl_const
const_add 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add InnerProductSpace.harmonicContOnCl_const
const_smul 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Real Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	InnerProductSpace.HarmonicOnNhd.const_smul harmonicOnNhd ContinuousOn.const_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul continuousOn
const_sub 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub InnerProductSpace.harmonicContOnCl_const
contDiffAt 📖	mathematical	InnerProductSpace.HarmonicContOnCl Set Set.instMembership	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	—	harmonicOnNhd
continuousOn 📖	mathematical	InnerProductSpace.HarmonicContOnCl	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup closure	—	—
continuousOn_ball 📖	mathematical	InnerProductSpace.HarmonicContOnCl Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Metric.closedBall	—	eq_or_ne Metric.closedBall_zero continuousOn_singleton closure_ball continuousOn
differentiableAt 📖	mathematical	InnerProductSpace.HarmonicContOnCl Set Set.instMembership	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	ContDiffAt.differentiableAt Nat.instAtLeastTwoHAddOfNat contDiffAt two_ne_zero CharZero.NeZero.two WithTop.charZero
fun_add 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add
fun_add_const 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add_const
fun_const_add 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	const_add
fun_const_smul 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	const_smul
fun_const_sub 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	const_sub
fun_neg 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg
fun_sub 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub
fun_sub_const 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub_const
harmonicOnNhd 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicOnNhd	—	—
mk_ball 📖	mathematical	InnerProductSpace.HarmonicOnNhd Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Metric.closedBall	InnerProductSpace.HarmonicContOnCl Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContinuousOn.mono Metric.closure_ball_subset_closedBall
mono 📖	mathematical	InnerProductSpace.HarmonicContOnCl Set Set.instHasSubset	InnerProductSpace.HarmonicContOnCl	—	InnerProductSpace.HarmonicOnNhd.mono harmonicOnNhd ContinuousOn.mono continuousOn closure_mono
neg 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	InnerProductSpace.HarmonicOnNhd.neg harmonicOnNhd ContinuousOn.neg IsTopologicalAddGroup.toContinuousNeg SeminormedAddCommGroup.toIsTopologicalAddGroup continuousOn
sub 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	InnerProductSpace.HarmonicOnNhd.sub harmonicOnNhd ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousOn
sub_const 📖	mathematical	InnerProductSpace.HarmonicContOnCl	InnerProductSpace.HarmonicContOnCl Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub InnerProductSpace.harmonicContOnCl_const

InnerProductSpace.HarmonicOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonicContOnCl 📖	mathematical	InnerProductSpace.HarmonicOnNhd closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	InnerProductSpace.HarmonicContOnCl	—	mono subset_closure continuousOn

InnerProductSpace.IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonicContOnCl_iff 📖	mathematical	—	InnerProductSpace.HarmonicContOnCl InnerProductSpace.HarmonicOnNhd	—	InnerProductSpace.HarmonicContOnCl.harmonicOnNhd InnerProductSpace.HarmonicOnNhd.harmonicContOnCl IsClosed.closure_eq

---

← Back to Index