Обсуждение:Евклидова геометрия

Untitled

Об аксиомах Евклидовой геометрии

1.1. Об отношениях между точками и прямыми

1.1.1 Каждые две точки принадлежат по меньшей мере одной прямой.

$~\forall A_{1}\ \forall A_{2}\ \exists \{1,...\}a\ (\langle A_{1},A_{2}\rangle \in a\times a)$

$~\Leftrightarrow \forall A_{1}\forall A_{2}\exists a\ (A_{1}\in a\ \land \ A_{2}\in a)$

Следствия

Каждая точка принадлежит по меньшей мере одной прямой.

$~\forall A\ \exists a\ (A\in a)$

$~\Leftrightarrow \forall A\ \exists \{1,...\}a\ (A\in a)$

Каждые две различные точки принадлежат по меньшей мере одной прямой.

$~\forall A_{1}\forall A_{2}\ (A_{1}\neq A_{2}\to \exists a\ (\langle A_{1},A_{2}\rangle \in a\times a))$

1.1.2 Каждые две различные точки принадлежат самое большее одной прямой.

$~\forall A_{1},A_{2}\ (A_{1}\neq A_{2}\to \exists \{0,1\}a\ (\langle A_{1},A_{2}\rangle \in a\times a))$

$~\Leftrightarrow \forall A_{1}\forall A_{2}\ (A_{1}\neq A_{2}\to \forall a_{1}\forall a_{2}\ (A_{1}\in a_{1}\ \land \ A_{2}\in a_{1}\quad \land \quad A_{1}\in a_{2}\ \land \ A_{2}\in a_{2}\to a_{1}=a_{2}))$

Следствие

Каждые две различные прямые пересекаются самое большее в одной точке.

$~\forall a_{1}\forall a_{2}\ (a_{1}\neq a_{2}\to \forall A_{1}\forall A_{1}\ (A_{1}\in a_{1}\ \land \ A_{1}\in a_{2}\quad \land \quad A_{2}\in a_{1}\ \land \ A_{2}\in a_{2}\to A_{1}=A_{2}))$

$~\Leftrightarrow \forall a_{1}\forall a_{2}\ (a_{1}\neq a_{2}\to \exists \{0,1\}A\ (A\in a_{1}\cap a_{2}))$

1.1.3 Какова бы ни была прямая, существуют по меньшей мере три точки, из которых одна [точка] не принадлежит данной прямой.

$~\forall a\ \exists A_{1},A_{2},A_{3}\ (A_{1}\neq A_{2}\ \land \ A_{1}\neq A_{3}\ \land \ A_{2}\neq A_{3}\quad \land \quad A_{1}\in a\ \land \ A_{2}\in a\ \land \ A_{3}\notin a)$

1.2. Об отношениях между точками и плоскостями

1.2.1 Если одна точка принадлежит двум плоскостям, тогда существует ещё одна точка, принадлежащая этим плоскостям.

$~\forall A_{1}\ \forall \alpha _{1}\ \forall \alpha _{2}\ (A_{1}\in \alpha _{1}\cap \alpha _{2}\to \exists A_{2}\ (A_{2}\neq A_{1}\ \land \ A_{2}\in \alpha _{1}\cap \alpha _{2}))$

1.2.2 Какова бы ни была плоскоть, существуют по меньшей мере четыре точки, из которых одна [точка] не принадлежит этой плоскости.

${\begin{aligned}\forall \alpha \ \exists A_{1},A_{2},A_{3},A_{4}\ (A_{1}\neq A_{2}\ \land \ A_{1}\neq A_{3}\ \land \ A_{1}\neq A_{4}\ \land \ A_{2}\neq A_{3}\ \land \ A_{2}\neq A_{4}\ \land \ A_{3}\neq A_{4}\\\ \land \ A_{1}\in \alpha \ \land \ A_{2}\in \alpha \ \land \ A_{3}\in \alpha \ \land \ A_{4}\notin \alpha )\end{aligned}}$

1.3. Об отношениях между точками, прямыми и плоскостями.

1.3.1.1 Каждые три точки, не лежащие на одной прямой, принадлежат по меньшей мере одной плоскости.

$~\forall A_{1},A_{2},A_{3}\ (\neg (\exists a\ (A_{1}\in a\ \land \ A_{2}\in a\ \land \ A_{3}\in a))\to \exists \alpha \ (A_{1}\in \alpha \ \land \ A_{2}\in \alpha \ \land \ A_{3}\in \alpha ))$

1.3.1.2 Каковы бы ни три точки, не лежащие на одной прямой, существует самое большее одна плоскость, которой они принадлежат.

$~\forall A_{1},A_{2},A_{3}\ (\neg (\exists a\ (A_{1}\in a\ \land \ A_{2}\in a\ \land \ A_{3}\in a))\to \exists \{0,1\}\alpha \ (A_{1}\in \alpha \ \land \ A_{2}\in \alpha \ \land \ A_{3}\in \alpha ))$

1.3.2 Если две различные точки принадлежат и одной прямой, и одной плоскости, тогда каждая точка этой прямой принадлежит этой плоскости.

$~\forall A_{1},A_{2}\ \forall a\ \forall \alpha \ (A_{1}\neq A_{2}\ \land \ A_{1}\in a\cap \alpha \ \land \ A_{2}\in a\cap \alpha \to \forall A\ (A\in a\to A\in \alpha ))$

1.3.3 Аксиома параллельности

$~\forall A\ \forall a\ \forall \alpha \ (A\in \alpha \ \land \ A\notin a\ \land \ a\subseteq \alpha \to \exists \{1\}a_{1}\ (A\in a_{1}\ \land \ a_{1}\subset \alpha \ \land \ a_{1}\cap a=\varnothing )$

2. О порядке

2.1 О порядке на прямой

2.1.1 Если точка $~A_{2}$, принадлежащая прямой $~a$, лежит между точками $~A_{1}$ и $~A_{3}$ этой же прямой, тогда точка $~A_{2}$ лежит между точками $~A_{3}$ и $~A_{1}$, при этом все эти точки попарно различны.

$~\forall a\ \forall A_{1},A_{2},A_{3}\ (A_{1},A_{2},A_{3}\in a\ \land \ \langle A_{1}|A_{2}|A_{3}\rangle \to \langle A_{3}|A_{2}|A_{1}\rangle \ \land \ A_{1}\neq A_{2}\ \land \ A_{1}\neq A_{3}\ \land \ A_{2}\neq A_{3})$

2.1.2 Каковы бы ни были две различные точки $~A_{1}$ и $~A_{2}$, найдётся такая точка $~A_{3}$, что $~A_{2}$ лежит между точками $~A_{1}$ и $~A_{3}$.

$~\forall A_{1},A_{2}\ \forall a\ (A_{1}\neq A_{2}\ \land \ A_{1}\in a\ \land \ A_{2}\in a\to \exists A_{3}\ (A_{3}\in a\ \land \ \langle A_{1}|A_{2}|A_{3}\rangle ))$

2.1.3 Среди любых трёх попарно различных точек одной прямой есть самое большее одна точка, которая лежит между двумя другими [точками].

${\begin{matrix}\forall A_{1},A_{2},A_{3}\ \forall a\ (A_{1}\neq A_{2}\ \land \ A_{1}\neq A_{3}\ \land \ A_{2}\neq A_{3}\ \land \ A_{1}\in a\ \land \ A_{2}\in a\ \land \ A_{3}\in a\quad \to \\\ \neg (\langle A_{1}|A_{3}|A_{2}\rangle \ \land \ \langle A_{1}|A_{2}|A_{3}\rangle \ \lor \ \langle A_{1}|A_{3}|A_{2}\rangle \ \land \ \langle A_{2}|A_{1}|A_{3}\rangle \ \lor \ \langle A_{1}|A_{2}|A_{3}\rangle \ \land \ \langle A_{2}|A_{1}|A_{3}\rangle ))\end{matrix}}$

2.2 Аксиома Паша

${\begin{aligned}\forall A_{1},A_{2},A_{3}\ \forall b\ (\neg (\exists a\ (A_{1}\in a\land A_{2}\in a\land A_{3}\in a))\ \land \ b\subset A_{1}A_{2}A_{3}\\\ \land \ A_{1}\notin b\ \land \ A_{2}\notin b\ \land \ A_{3}\notin b\ \land \ b\cap (A_{1}A_{2})\neq \varnothing \\\ \to b\cap (A_{2}A_{3})\neq \varnothing \ \veebar \ b\cap (A_{3}A_{1})\neq \varnothing )\end{aligned}}$

--Галактион 19:54, 5 февраля 2009 (UTC)