Displaying 101 – 120 of 1303

Showing per page

Algebraic Numbers

Yasushige Watase (2016)

Formalized Mathematics

This article provides definitions and examples upon an integral element of unital commutative rings. An algebraic number is also treated as consequence of a concept of “integral”. Definitions for an integral closure, an algebraic integer and a transcendental numbers [14], [1], [10] and [7] are included as well. As an application of an algebraic number, this article includes a formal proof of a ring extension of rational number field ℚ induced by substitution of an algebraic number to the polynomial...

All Liouville Numbers are Transcendental

Artur Korniłowicz, Adam Naumowicz, Adam Grabowski (2017)

Formalized Mathematics

In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 [15] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real...

Altitude, Orthocenter of a Triangle and Triangulation

Roland Coghetto (2016)

Formalized Mathematics

We introduce the altitudes of a triangle (the cevians perpendicular to the opposite sides). Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the orthocenter of a triangle [7]. Finally, we formalize in Mizar [1] some formulas [2] to calculate distance using triangulation.

Amenability, extreme amenability, model-theoretic stability, and dependence property in integral logic

Karim Khanaki (2016)

Fundamenta Mathematicae

This paper has three parts. First, we study and characterize amenable and extremely amenable topological semigroups in terms of invariant measures using integral logic. We prove definability of some properties of a topological semigroup such as amenability and the fixed point on compacta property. Second, we define types and develop local stability in the framework of integral logic. For a stable formula ϕ, we prove definability of all complete ϕ-types over models and deduce from this the fundamental...

An algebraic completeness proof for Kleene's 3-valued logic

Maurizio Negri (2002)

Bollettino dell'Unione Matematica Italiana

We introduce Kleene's 3-valued logic in a language containing, besides the Boolean connectives, a constant n for the undefined truth value, so in developing semantics we can switch from the usual treatment based on DM-algebras to the narrower class of DMF-algebras (De Morgan algebras with a single fixed point for negation). A sequent calculus for Kleene's logic is introduced and proved complete with respect to threevalent semantics. The completeness proof is based on a version of the prime ideal...

An axiom system for full 3 -dimensional Euclidean geometry

Jarosław Kosiorek (1991)

Mathematica Bohemica

We present an axiom system for class of full Euclidean spaces (i.e. of projective closures of Euclidean spaces) and prove the representation theorem for our system, using connections between Euclidean spaces and elliptic planes.

Currently displaying 101 – 120 of 1303