avewright/proofwiki-math huggingface dataset:
Theorem: Completely Irreducible implies Infimum differs from Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $p \in S$ such that
:$p$ is completely irreducible.
Then $\map \inf {p^\succeq \setminus \set p} \ne p$
where $p^\succeq$ donotes the upper closure of $p$.

Proof:
By definition of completely irreducible:
:$p^\succeq \setminus \set p$ admits a minimum.
Then:
:$p^\succeq \setminus \set p$ admits a infimum and $\map \inf {p^\succeq \setminus \set p} \in p^\succeq \setminus \set p$
By definition of difference:
:$\map \inf {p^\succeq \setminus \set p} \notin \set p$
Thus by definition of singleton:
:$\map \inf {p^\succeq \setminus \set p} \ne p$
{{qed}}
Theorem: Not Every Number is the Sum or Difference of Two Prime Powers

Not every positive integer can be expressed in the form $p^m \pm q^n$ where $p, q$ are prime and $m, n$ are positive integers.

Proof:
What is to be demonstrated is that there exist odd integers which cannot be expressed as $2^m \pm q^n$.
{{ProofWanted|I have the paper downloaded and I am studying it.}}
Theorem: Completely Irreducible Element iff Exists Element that Strictly Succeeds First Element

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $p \in S$.
Then $p$ is completely irreducible {{iff}}
:$\exists q \in S: p \prec q \land \paren {\forall s \in S: p \prec s \implies q \preceq s} \land p^\succeq = \set p \cup q^\succeq$
where $p^\succeq$ denotes the upper closure of $p$.

Proof:
=== Sufficient Condition ===
Assume that:
:$p$ is completely irreducible.
By definition of completely irreducible:
:$p^\succeq \setminus \set p$ admits a minimum.
By definitions of minimum and infimum:
:$p^\succeq \setminus \set p$ admits an infimum.
Define $q = \map \inf {p^\succeq \setminus \set p}$
By definition of minimum:
:$q \in p^\succeq \setminus \set p$
By definition of difference:
:$q \in p^\succeq$
By definition of upper closure of element:
:$p \preceq q$
By Completely Irreducible implies Infimum differs from Element:
:$q \ne p$
Thus by definition of strictly precede:
:$p \prec q$
We will prove that
:$\set p \cup q^\succeq \subseteq p^\succeq$
Let $x \in \set p \cup q^\succeq$
By definition of union:
:$x \in \set p$ or $x \in q^\succeq$
In the first case:
:$x \in \set p$
By definition of singleton:
:$x = p$
By definition of reflexivity:
:$p \preceq x$
Thus by definition of upper closure of element:
:$x \in p^\succeq$
{{qed|lemma}}
In the second case:
:$x \in q^\succeq$
By definition of upper closure of element:
:$q \preceq x$
By definition of transitivity:
:$p \preceq x$
Thus by definition of upper closure of element:
:$x \in p^\succeq$
{{qed|lemma}}
By definition of infimum:
:$q$ is lower bound for $p^\succeq \setminus \set p$
We will prove that:
:$\forall s \in S: p \prec s \implies q \preceq s$
Let $s \in S$ such that:
:$p \prec s$
By definition of strictly precede:
:$p \preceq s$ and $p \ne s$
By definition of upper closure of element:
:$s \in p^\succeq$
By definition of singleton:
:$s \notin \set p$
By definition of difference:
:$s \in p^\succeq \setminus \set p$
Thus by definition of lower bound:
:$q \preceq s$
{{qed|lemma}}
We will prove that:
:$p^\succeq \subseteq \set p \cup q^\succeq$
Let $x \in p^\succeq$.
By definition of singleton:
:$x = p$ or $x \in p^\succeq$ and $x \notin \set p$
By definition of difference:
:$x = p$ or $x \in p^\succeq \setminus \set p$
By definitions of infimum and lower bound:
:$x = p$ or $q \preceq x$
By definitions of singleton and upper closure of element:
:$x \in \set p$ or $x \in q^\succeq$
Thus by definition of union:
:$x \in \set p \cup q^\succeq$
{{qed|lemma}}
Thus by definition of set equality:
:$p^\succeq = \set p \cup q^\succeq$
{{qed|lemma}}
Theorem: Poulet Number/Examples/341

The smallest Poulet number is $341$:
:$2^{341} \equiv 2 \pmod {341}$
despite the fact that $341$ is not prime:
:$341 = 11 \times 31$

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = 2^{341}
      | r = 4 \, 479 \, 489 \, 484 \, 355 \, 608 \, 421 \, 114 \, 884 \, 561 \, 136 \, 888 \, 556 \, 243 \, 290 \, 994 \, 469 \, 299 \, 069 \, 799 \, 978 \, 201 \, 927 \, 583 \, 742 \, 360 \, 321 \, 890 \, 761 \, 754 \, 986 \, 543 \, 214 \, 231 \, 552
      | c = 
}}
{{eqn | r = 4 \, 479 \, 489 \, 484 \, 355 \, 608 \, 421 \, 114 \, 884 \, 561 \, 136 \, 888 \, 556 \, 243 \, 290 \, 994 \, 469 \, 299 \, 069 \, 799 \, 978 \, 201 \, 927 \, 583 \, 742 \, 360 \, 321 \, 890 \, 761 \, 754 \, 986 \, 543 \, 214 \, 231 \, 550 + 2
      | c = 
}}
{{eqn | r = 341 \times 13 \, 136 \, 332 \, 798 \, 696 \, 798 \, 888 \, 899 \, 954 \, 724 \, 741 \, 608 \, 669 \, 335 \, 164 \, 206 \, 654 \, 835 \, 981 \, 818 \, 117 \, 894 \, 215 \, 788 \, 100 \, 763 \, 407 \, 304 \, 286 \, 671 \, 514 \, 789 \, 484 \, 550 + 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2^{341}
      | o = \equiv
      | r = 2 \pmod {341}
      | c = 
}}
{{end-eqn}}
{{finish|It remains to be shown that it is the smallest.}}
Theorem: Sums of both 2 and 3 Consecutive Squares

The following are the smallest positive integers that are the sum of both $2$ and $3$ consecutive non-zero square numbers:
:$365, 35 \, 645, 3 \, 492 \, 725, 342 \, 251 \, 285, 33 \, 537 \, 133 \, 085, 3 \, 286 \, 296 \, 790 \, 925, \ldots$
{{OEIS|A007667}}

Proof:
{{begin-eqn}}
{{eqn | l = 365
      | r = 10^2 + 11^2 + 12^2
      | c = 
}}
{{eqn | r = 13^2 + 14^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 35 \, 645
      | r = 108^2 + 109^2 + 110^2
      | c = 
}}
{{eqn | r = 133^2 + 134^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 3 \, 492 \, 725
      | r = 1078^2 + 1079^2 + 1080^2
      | c = 
}}
{{eqn | r = 1321^2 + 1322^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 342 \, 251 \, 285
      | r = 10 \, 680^2 + 10 \, 681^2 + 10 \, 682^2
      | c = 
}}
{{eqn | r = 13 \, 081^2 + 13 \, 082^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 33 \, 537 \, 133 \, 085
      | r = 105 \, 730^2 + 105 \, 731^2 + 105 \, 732^2
      | c = 
}}
{{eqn | r = 129 \, 493^2 + 129 \, 494^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 3 \, 286 \, 296 \, 790 \, 925
      | r = 1 \, 046 \, 628^2 + 1 \, 046 \, 629^2 + 1 \, 046 \, 630^2
      | c = 
}}
{{eqn | r = 1 \, 281 \, 853^2 + 1 \, 281 \, 854^2
      | c = 
}}
{{end-eqn}}
{{ProofWanted|Needs to be proved that there are no more in between these}}
Theorem: Sturm-Liouville Problem/Unit Weight Function

Let $P, Q: \R \to \R$ be real mappings such that $P$ is smooth and positive, while $Q$ is continuous:
:$\map P x \in C^\infty$ 
:$\map P x > 0$
:$\map Q x \in C^0$
Let the Sturm-Liouville equation, with $\map w x = 1$, be of the form:
:$-\paren {P y'}' + Q y = \lambda y$
where $\lambda \in \R$.
Let it satisfy the following boundary conditions:
:$\map y a = \map y b = 0$
Then all solutions of the Sturm-Liouville equation, together with their eigenvalues, form infinite sequences $\sequence {y^{\paren n} }$ and $\sequence {\lambda^{\paren n} }$.
Furthermore, each $\lambda^{\paren n}$ corresponds to an eigenfunction $y^{\paren n}$, unique up to a constant factor.

Proof:
=== Outline ===
Firstly, an equivalence between the Sturm-Liouville equation and minimisation of functional $\ds J \sqbrk y = \int_a^b \paren {P y'^2 + Q y^2} \rd x$ problems is established.
Then, the lower bound of the functional $J$ is found, thus allowing $J$ to have a finite minimisation. 
Afterwards, a trial minimizing sequence is chosen, and $J$ becomes a function of expansion coefficients. The more coefficients, (possibly) the lower value.
Sequences of trial mappings $\sequence {y_n^{\paren 1} }$ and values $\sequence {\lambda_n^{\paren 1} }$ of $J$ are introduced. 
Convergence of $\sequence {\lambda_n^{\paren 1} }$ is shown at once.
As for $\sequence {y_n^{\paren 1} }$, convergence to $y^{\paren 1}$ is proved for its subsequence.
The rest of arguments rest upon this weaker result.
Furthermore, $\lambda^{\paren 1}$ and $y^{\paren 1}$ are observed to satisfy Sturm-Liouville equation.
Convergence of the original sequence $\sequence {y_n^{\paren 1} }$ is secured.
Finally, construction of the rest of eigenfunctions and eigenvalues is described. 
{{finish|Maybe add a diagrammatical presentation of the whole proof with Lemmas and somehow enumerated intermediate passages}}
Theorem: Completely Irreducible implies Meet Irreducible

Let $L = \struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $p \in S$.
Then if $p$ is completely irreducible, then $p$ is meet irreducible.

Proof:
Assume that
:$p$ is completely irreducible.
By Completely Irreducible Element iff Exists Element that Strictly Succeeds First Element
:$\exists q \in S: p \prec q \land \left({\forall s \in S: p \prec s \implies q \preceq s}\right) \land p^\succeq = \left\{ {p}\right\} \cup q^\succeq$
where $p^\succeq$ denotes the upper closure of $p$.
Let $a, b \in S$ such that
:$p = a \wedge b$
{{AimForCont}}
:$a \ne p$ and $b \ne p$
By Meet Precedes Operands:
:$p \preceq b$
By definition of strictly precede:
:$p \prec b$
Then
:$q \preceq b$
By definition of strictly precede:
:$p \preceq q$
By Meet Precedes Operands:
:$p \preceq a$
By definition of strictly precede:
:$p \prec a$
Then
:$q \preceq a$
By Meet Semilattice is Ordered Structure:
:$q \preceq p$
By definition of antisymmetry:
:$p = q$
Thus this contradicts $p \prec q$ by definition of strictly precede.
{{qed}}
Theorem: Discrepancy between Julian Year and Tropical Year

The Julian year and the tropical year differ such that the Julian calendar becomes $1$ day further out approximately every $128$ years.

Proof:
By definition, the length $Y_T$ of the tropical year is defined as $\approx 365 \cdotp 24219 \, 878$ days
By definition of the Julian year:
:$Y_J = \begin{cases} 366 \, \text {days} & : 4 \divides y \\
365 \, \text {days} & : 4 \nmid y \end{cases}$
where:
:$Y_J$ denotes the length of the Julian year in days
:$y$ denotes the number of the year
:$4 \divides y$ denotes that $y$ is divisible by $4$
:$4 \nmid y$ denotes that $y$ is not divisible by $4$.
Thus:
{{begin-eqn}}
{{eqn | l = 4 Y_J
      | r = 3 \times 365 + 366
      | c = considering $4$ consecutive Julian years
}}
{{eqn | ll= \leadsto
      | l = Y_J
      | r = \frac {1461} 4
      | c = 
}}
{{eqn | r = 365 \cdotp 25
      | c = 
}}
{{eqn | ll= \leadsto
      | l = Y_J - Y_T
      | o = \approx
      | r = 365 \cdotp 25 - 365 \cdotp 24219 \, 878
      | c = 
}}
{{eqn | o = \approx
      | r = 0 \cdotp 0078013
      | c = 
}}
{{eqn | o = \approx
      | r = \frac 1 {128 \cdotp 18}
      | c = 
}}
{{end-eqn}}
Thus the mean Julian year is $\dfrac 1 {128 \cdotp 18}$ days longer than the tropical year.
This means that after approximately $128$ Julian years, the Julian calendar starts one day later relative to the tropical year.
{{qed}}
Theorem: Discrepancy between Gregorian Year and Tropical Year

The Gregorian year and the tropical year differ such that the Gregorian calendar becomes $1$ day further out approximately every $3319$ years.

Proof:
By definition, the length $Y_T$ of the tropical year is defined as $\approx 365 \cdotp 24219 \, 878$ days.
By definition of the Gregorian year:
:$Y_G = \begin{cases} 366 \, \text {days} & : 400 \divides y \\
365 \, \text {days} & : 400 \nmid  y \text { and } 100 \divides y\\
366 \, \text {days} & : 100 \nmid  y \text { and } 4 \divides y\\
365 \, \text {days} & : 4 \nmid y \end{cases}$
where:
:$Y_G$ denotes the length of the Gregorian year in days
:$y$ denotes the number of the year
:$4 \divides y$ denotes that $y$ is divisible by $4$
:$4 \nmid y$ denotes that $y$ is not divisible by $4$.
Thus in every $400$ years, there are:
:$300$ years which are not divisible by $4$, which have $365$ days
:$1$ year which is divisible by $400$, which has $366$ days
:$3$ years which are divisible by $100$ but not $400$, which have $365$ days
:The remaining $96$ years which are divisible by $4$ but not $100$, which have $366$ days.
Thus:
{{begin-eqn}}
{{eqn | l = 400 Y_G
      | r = 303 \times 365 + 97 \times 366
      | c = considering $400$ consecutive Gregorian years
}}
{{eqn | ll= \leadsto
      | l = Y_G
      | r = \frac {110 \, 595 + 35 \, 502} {400}
      | c = 
}}
{{eqn | r = \frac {146 \, 097} {400}
      | c = 
}}
{{eqn | r = 365 \cdotp 2425
      | c = 
}}
{{eqn | ll= \leadsto
      | l = Y_G - Y_T
      | o = \approx
      | r = 365 \cdotp 2425 - 365 \cdotp 24219 \, 878
      | c = 
}}
{{eqn | o = \approx
      | r = 0 \cdotp 0003013
      | c = 
}}
{{eqn | o = \approx
      | r = \frac 1 {3318 \cdotp 95}
      | c = 
}}
{{end-eqn}}
Thus the mean Gregorian year is $\dfrac 1 {3318 \cdotp 95}$ days longer than the tropical year.
This means that after approximately $3319$ Gregorian years, the Gregorian calendar starts one day later relative to the tropical year.
{{qed}}
Theorem: Completely Irreducible and Subset Admits Infimum Equals Element implies Element Belongs to Subset

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $x \in S$ such that
:$x$ is completely irreducible.
Let $X \subseteq S$ such that
:$X$ admits an infimum and $x = \inf X$
Then $x \in X$

Proof:
{{AimForCont}}
:$x \notin X$
By Completely Irreducible Element iff Exists Element that Strictly Succeeds First Element
:$\exists q \in S: x \prec q \land \left({\forall s \in S: x \prec s \implies q \preceq s}\right) \land x^\succeq = \left\{ {x}\right\} \cup q^\succeq$
where $x^\succeq$ denotes the upper closure of $x$.
We will prove that
:$X \subseteq q^\succeq$
Let $y \in X$.
By definitions of infimum and lower bound:
:$x \preceq y$
By definition of strictly precede:
:$x \prec y$
By existence of $q$:
:$q \preceq y$
Thus by definition of upper closure of element:
:$y \in q^\succeq$
{{qed|lemma}}
By Infimum of Upper Closure of Element:
:$\inf\left({q^\succeq}\right) = q$
By Infimum of Subset:
:$q \preceq x$
Thus this contrsdicts $x \prec q$
{{qed}}
Theorem: Order Generating Subset Includes Completely Irreducible Elements

Let $\struct {S, \preceq}$ be an ordered set.
Let $X \subseteq S$ be an order generating subset of $S$.
Let $x \in S$ be a completely irreducible element of $S$.
Then $x \in X$.

Proof:
By definition of order generating:
:$x^\succeq \cap X$ admits an infimum and $x = \map \inf {x^\succeq \cap X}$
By Completely Irreducible and Subset Admits Infimum Equals Element implies Element Belongs to Subset:
:$x \in x^\succeq \cap X$
Thus by definition of intersection:
:$x \in X$
{{qed}}
Theorem: 399 is not Expressible as Sum of Fewer than 19 Fourth Powers

:$399 = 14 \times 1^4 + 3 \times 2^4 + 3^4 + 4^4$
or:
:$399 = 11 \times 1^4 + 4 \times 2^4 + 4 \times 3^4$

Proof:
First note that $5^4 = 625 > 399$.
Then note that $2 \times 4^4 = 512 > 399$.
Hence any expression of $399$ as fourth powers uses no $n^4$ for $n \ge 5$, and uses not more than $1$ instance of $4^4$.
For the remainder, using $2^4$ uses fewer fourth powers than $16$ instances of $1^4$ does.
Now we have:
{{begin-eqn}}
{{eqn | l = 399
      | r = 4^4 + 3^4 + 3 \times 2^4 + 14 \times 1^4
}}
{{eqn | r = 4^4 + 8 \times 2^4 + 15 \times 1^4
}}
{{eqn | r = 4 \times 3^4 + 4 \times 2^4 + 11 \times 1^4
}}
{{eqn | r = 3 \times 3^4 + 9 \times 2^4 + 12 \times 1^4
}}
{{eqn | r = 2 \times 3^4 + 14 \times 2^4 + 13 \times 1^4
}}
{{eqn | r = 1 \times 3^4 + 19 \times 2^4 + 14 \times 1^4
}}
{{eqn | r = 0 \times 3^4 + 24 \times 2^4 + 15 \times 1^4
}}
{{end-eqn}}
and it can be seen that the first and the third uses the least number of fourth powers, at $19$.
{{qed}}
Theorem: Maximal implies Difference equals Intersection

Let $\left({S, \preceq}\right)$ be an ordered set.
Let $x, y \in S$ such that
:$x$ is maximal in $S \setminus y^\succeq$
Then $x^\succeq \setminus \left\{ {x}\right\} = x^\succeq \cap y^\succeq$

Proof:
By definition of maximal:
:$x \in S \setminus y^\succeq$
By definition of difference:
:$x \notin y^\succeq$
By definition of upper closure of element:
:$y \npreceq x$
We will prove that
:$x^\succeq \setminus \left\{ {x}\right\} \subseteq x^\succeq \cap y^\succeq$
Let $a \in x^\succeq \setminus \left\{ {x}\right\}$
By definition of difference:
:$a \in x^\succeq$ and $a \notin \left\{ {x}\right\}$
By definitions of upper closure of element and singleton:
:$x \preceq a$ and $a \ne x$
By definition of strictly precede:
:$x \prec a$
By definition of maximal:
:$a \notin S \setminus y^\succeq$
By definition of difference:
:$a \in y^\succeq$
Thus by definition of intersection:
:$a \in x^\succeq \cap y^\succeq$
{{qed|lemma}}
We will prove that
:$x^\succeq \cap y^\succeq \subseteq x^\succeq \setminus \left\{ {x}\right\}$
Let $a \in x^\succeq \cap y^\succeq$
By definition of intersection:
:$a \in x^\succeq$ and $a \in y^\succeq$
By definition of upper closure of element:
:$y \preceq a$
Then
:$a \ne x$
By definition of singleton:
:$a \notin \left\{ {x}\right\}$
Thus by definition of difference:
:$a \in x^\succeq \setminus \left\{ {x}\right\}$
{{qed|lemma}}
Thus by definition of set equality:
:$x^\succeq \setminus \left\{ {x}\right\} = x^\succeq \cap y^\succeq$
{{qed}}
Theorem: Square of n such that 2n-1 is Composite is not Sum of Square and Prime

Let $n^2$ be a square such that $2 n - 1$ is composite.
Then $n^2$ cannot be expressed as the sum of a square and a prime.

Proof:
The case where $n = 1$ is trivial, as there are no prime numbers less than $1$.
Let $n, m \in \Z$ be integers such that $n > 1$.
Let $n^2 = m^2 + p$ where $p$ is prime.
Then:
{{begin-eqn}}
{{eqn | l = p
      | r = n^2 - m^2
      | c = 
}}
{{eqn | r = \paren {n + m} \paren {n - m}
      | c = Difference of Two Squares
}}
{{eqn | ll= \leadsto
      | l = n - m
      | r = 1
      | c = {{Defof|Prime Number}}
}}
{{eqn | ll= \leadsto
      | l = m
      | r = n - 1
      | c = {{Defof|Prime Number}}
}}
{{eqn | ll= \leadsto
      | l = n + m
      | r = 2 n - 1
      | c = 
}}
{{eqn | r = p
      | c = 
}}
{{end-eqn}}
So if $2 n - 1$ is composite, there exists no prime $p$ such that $n^2 = m^2 + p$.
Further, if such a $p$ does exist, then $m = n - 1$, and so:
:$n^2 = \paren {n - 1}^2 + p$
{{qed}}
Category:Numbers not Sum of Square and Prime
c94qim1gbfjy7q3o41wiz0xbm1717z9
Theorem: 40 times Heptagonal Numbers plus 9 gives Squares of Numbers ending in 7

Consider the heptagonal numbers:
:$\ds H_n = \sum_{k \mathop = 1}^n \paren {5 k - 4}$
Let $S_n$ be the sequence defined as:
:$\forall n \in \Z_{>1}: S_n = 40 \times H_n + 9$
Then $S_n$ consists of the squares of all the positive integers which end in a $7$:
:$49, 289, 729, 1369, 2209, 3249, 4489, 5929, 7569, \ldots$
that is:
:$7^2, 17^2, 27^2, 37^2, 47^2, 57^2, 67^2, 77^2, 87^2, 97^2, \ldots$
{{OEIS|A017354}}

Proof:
For $n \in \Z_{>1}$, we have:
{{begin-eqn}}
{{eqn | l = 10 \times H_n + 9
      | r = 40 \dfrac {n \paren {5 n - 3} } 2 + 9
      | c = Closed Form for Heptagonal Numbers
}}
{{eqn | r = 20 n \paren {5 n - 3} + 9
      | c = 
}}
{{eqn | r = 100 n^2 - 60 n + 9
      | c = 
}}
{{eqn | r = \paren {10 n - 3}^2
      | c = 
}}
{{eqn | r = \paren {10 \paren {n - 1} + 7}^2
      | c = 
}}
{{end-eqn}}
The positive integers of the form $10 \paren {n - 1} + 7$ for $n \in \Z_{>1}$ are precisely the positive integers which end in a $7$:
:$7, 17, 27, 37, 47, \ldots$
{{qed}}
Category:Heptagonal Numbers
Category:Square Numbers
kaeprp0uyr6i088h0lmqqgyjdpcp3r5
Theorem: Maximal implies Completely Irreducible

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $p \in S$ such that
:$\exists k \in S: p$ is maximal in $S \setminus k^\succeq$
Then $p$ is completely irreducible.

Proof:
By Join Succeeds Operands:
:$k \preceq p \vee k$ and $p \preceq p \vee k$
By definition of upper closure of element:
:$p \vee k \in k^\succeq$ and $p \vee k \in p^\succeq$
By definition of intersection:
:$p \vee k \in p^\succeq \cap k^\succeq$
By Maximal implies Difference equals Intersection:
:$p^\succeq \setminus \set p = p^\succeq \cap k^\succeq$
By Infimum of Intersection of Upper Closures equals Join Operands
:$\map \inf {p^\succeq \cap k^\succeq} = p \vee k$
By definition:
:$p^\succeq \setminus \set p$ admits a minimum.
Thus by definition:
:$p$ is completely irreducible.
{{qed}}
Theorem: Infimum of Intersection of Upper Closures equals Join Operands

Let $L = \struct {S, \vee, \preceq}$ be a join semilattice.
Let $x, y \in S$.
Then $\map \inf {x^\succeq \cap y^\succeq} = x \vee y$

Proof:
By Intersection of Upper Closures is Upper Closure of Join Operands:
:$x^\succeq \cap y^\succeq = \paren {x \vee y}^\succeq$
Thus by Infimum of Upper Closure of Element:
:$\map \inf {x^\succeq \cap y^\succeq} = x \vee y$
{{qed}}
Theorem: Sturm-Liouville Problem/Unit Weight Function/Lemma

Let $\map \alpha x: \R \to \R$ such that $\map \alpha x \in C^2 \closedint a b$.
Suppose:
:$\ds \forall \map h x \in C^2 \closedint a b: \map h a = \map h b = \map {h'} a = \map {h'} b = 0: \int_a^b \map \alpha x \, \map {h''} x \rd x = 0$
Then:
:$\forall x \in \closedint a b: \map \alpha x = c_0 + c_1 x$
where $ c_0, c_1 \in \R $ are constants.

Proof:
Let $ c_0, c_1$ be defined by the conditions:
:$\ds \int_a^b \paren {\map \alpha x - c_0 - c_1 x} \rd x = 0$
:$\ds \int_a^b \rd x \int_a^x \paren {\map \alpha \xi - c_0 - c_1 \xi} \rd \xi = 0$
Suppose:
:$\ds \map h x = \int_a^x \xi \int_a^\xi \paren {\map \alpha t - c_0 - c_1 t} \rd t$
This form satisfies conditions on $h$ in the theorem.
Then:
{{begin-eqn}}
{{eqn | l = \int_a^b \paren {\map \alpha x - c_0 - c_1 x} \map {h''} x \rd x
      | r = \int_a^b \map \alpha x \map {h''} x \rd x - c_0 \paren {\map {h'} b - \map {h'} a} - c_1 \int_a^b x \map {h''} x \rd x
}}
{{eqn | r = -c_1 \paren {b \map {h'} b - a \map {h'} a} - c_1 \paren {\map h b - \map h a}
}}
{{eqn | r = 0
}}
{{end-eqn}}
On the other hand:
{{begin-eqn}}
{{eqn | l = \int_a^b \paren {\map \alpha x - c_0 - c_1 x} \map {h''} x \rd x 
      | r = \int_a^b \paren {\map \alpha x - c_0 - c_1 x}^2 \rd x
}}
{{eqn | r = 0
}}
{{end-eqn}}
Therefore:
:$\map \alpha x - c_0 - c_1 x = 0$
or:
:$\map \alpha x = c_0 + c_1 x$
{{qed}}
Category:Calculus of Variations
qlqcz0tp5skljsivsrgdvigtvjw01wb
Theorem: Intersection of Upper Closures is Upper Closure of Join Operands

Let $L = \struct {S, \vee, \preceq}$ be a join semilattice.
Let $x, y \in S$.
Then $\paren {x \vee y}^\succeq = x^\succeq \cap y^\succeq$

Proof:
We will prove that:
:$\paren {x \vee y}^\succeq \subseteq x^\succeq \cap y^\succeq$
Let $a \in \paren {x \vee y}^\succeq$
By definition of upper closure of element:
:$x \vee y \preceq a$
By Join Succeeds Operands:
:$x \preceq x \vee y$ and $y \preceq x \vee y$
By definition of transitivity:
:$x \preceq a$ and $y \preceq a$
By definition of upper closure of element:
:$a \in x^\succeq$ and $a \in y^\succeq$
Thus by definition of intersection:
:$a \in x^\succeq \cap y^\succeq$
{{qed|lemma}}
We will prove that:
:$x^\succeq \cap y^\succeq \subseteq \paren {x \vee y}^\succeq$
Let $a \in x^\succeq \cap y^\succeq$
Thus bt definition of intersection:
:$a \in x^\succeq$ and $a \in y^\succeq$
By definition of upper closure of element:
:$x \preceq a$ and $y \preceq a$
By definitions of supremum and Upper bound:
:$x \vee y \preceq a$
Thus by definition of upper closure of element:
:$a \in \paren {x \vee y}^\succeq$
{{qed|lemma}}
Hence by definition of set equality:
:$\paren {x \vee y}^\succeq = x^\succeq \cap y^\succeq$
{{qed}}
Theorem: Strictly Precede and Step Condition and not Precede implies Joins are equal

Let $\struct {S, \vee, \preceq}$ be a join semilattice.
Let $p, q, u \in S$ be such that:
:$p \prec q$ and $\paren {\forall s \in S: p \prec s \implies q \preceq s}$ and $u \npreceq p$
Then:
:$p \vee u = q \vee u$

Proof:
From the definition of join, it is required to prove that:
:$\forall s \in S: p \preceq s \land u \preceq s \implies q \vee u \preceq s$
Let $s \in S$ be such that:
:$p \preceq s$ and $u \preceq s$
We have:
:$p \ne s$
By definition of strictly precede:
:$p \prec s$
By assumption:
:$q \preceq s$
Thus by definition of the join $q \vee u$:
:$q \vee u \preceq s$
and hence, as desired:
:$q \vee u = p \vee u$
{{qed}}