Liouville

Statistics

Metric	Count
Definitions	0
Theorems `bounded_harmonic_on_complex_plane_is_constant`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`bounded_harmonic_on_complex_plane_is_constant` 📖	—	`HarmonicOnNhd` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instFiniteDimensionalReal` `Set.univ` `Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range`	—	—	`Complex.instFiniteDimensionalReal` `exists_dual_vector''` `Set.range_comp` `Bornology.IsBounded.image` `ContinuousLinearMap.instLocallyBoundedMapClass` `RingHomIsometric.ids` `sub_eq_zero` `norm_eq_zero` `RCLike.ofReal_real_eq_id` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`

---