scholarly journals Decidable fan theorem and uniform continuity theorem with continuous moduli

2021 ◽  
Author(s):  
Makoto Fujiwara ◽  
Tatsuji Kawai
Keyword(s):  
Uniform Continuity ◽  
Continuity Theorem ◽  
Fan Theorem

scholarly journals Validating Brouwer's continuity principle for numbers using named exceptions

2017 ◽  
Vol 28 (6) ◽  
pp. 942-990 ◽  
Author(s):  
VINCENT RAHLI ◽  
MARK BICKFORD
Keyword(s):  
Equivalence Relation ◽  
Dependent Types ◽  
Proof Assistant ◽  
Continuity Theorem ◽  
Continuity Principle ◽  
Fan Theorem ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Intuitionistic Mathematics ◽  
Excluded Middle

This paper extends the Nuprl proof assistant (a system representative of the class of extensional type theories with dependent types) withnamed exceptionsandhandlers, as well as a nominalfreshoperator. Using these new features, we prove a version of Brouwer's continuity principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl's metatheory using our formalization of Nuprl in Coq and reflect these metatheoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl's key metatheoretical properties, in particular consistency and the congruence of Howe's computational equivalence relation. Using continuity and the fan theorem, we prove important results of Intuitionistic Mathematics: Brouwer's continuity theorem, bar induction on monotone bars and the negation of the law of excluded middle.

The pseudocompactness of [0.1] is equivalent to the uniform continuity theorem

2007 ◽  
Vol 72 (4) ◽  
pp. 1379-1384 ◽  
Author(s):  
Douglas Bridges ◽  
Hannes Diener
Keyword(s):  
Metric Space ◽  
Continuous Mapping ◽  
Uniform Continuity ◽  
Compact Metric Space ◽  
Continuity Theorem ◽  
Continuous Mappings ◽  
Necessary And Sufficient ◽  
Equivalent Conditions

AbstractWe prove constructively that, in order to derive the uniform continuity theorem for pointwise continuous mappings from a compact metric space into a metric space, it is necessary and sufficient to prove any of a number of equivalent conditions, such as that every pointwise continuous mapping of [0, 1] into ℝ is bounded. The proofs are analytic, making no use of, for example, fan-theoretic ideas.

scholarly journals Existence of weak solutions to SPDEs with fractional Laplacian and non-Lipschitz coefficients

2021 ◽  
Author(s):  
Shohei Nakajima
Keyword(s):  
Partial Differential Equations ◽  
Differential Equations ◽  
Weak Solutions ◽  
Stochastic Partial Differential Equations ◽  
Fractional Laplacian ◽  
Existence Of Solutions ◽  
Partial Differential ◽  
Continuity Theorem ◽  
Existence Of Weak Solutions ◽  
One Dimensional

AbstractWe prove existence of solutions and its properties for a one-dimensional stochastic partial differential equations with fractional Laplacian and non-Lipschitz coefficients. The method of proof is eatablished by Kolmogorov’s continuity theorem and tightness arguments.

Sign in / Sign up

Export Citation Format

Share Document