ProofNet

Rudin|exercise_1_1b

If $r$ is rational $(r \neq 0)$ and $x$ is irrational, prove that $rx$ is irrational.

\begin{proof} If $r x$ were rational, then $x=\frac{r x}{r}$ would also be rational. \end{proof}

theorem exercise_1_1b (x : ℝ) (y : ℚ) (h : y ≠ 0) : ( irrational x ) -> irrational ( x * y ) :=

import .common open real complex open topological_space open filter open_locale real open_locale topology open_locale big_operators open_locale complex_conjugate open_locale filter noncomputable theory

Rudin|exercise_1_4

Let $E$ be a nonempty subset of an ordered set; suppose $\alpha$ is a lower bound of $E$ and $\beta$ is an upper bound of $E$. Prove that $\alpha \leq \beta$.

\begin{proof} Since $E$ is nonempty, there exists $x \in E$. Then by definition of lower and upper bounds we have $\alpha \leq x \leq \beta$, and hence by property $i i$ in the definition of an ordering, we have $\alpha<\beta$ unless $\alpha=x=\beta$. \end{proof}

theorem exercise_1_4 (α : Type*) [partial_order α] (s : set α) (x y : α) (h₀ : set.nonempty s) (h₁ : x ∈ lower_bounds s) (h₂ : y ∈ upper_bounds s) : x ≤ y :=

import .common open real complex open topological_space open filter open_locale real open_locale topology open_locale big_operators open_locale complex_conjugate open_locale filter noncomputable theory