antisymm — Mathlib

English

Let A and B be subsets of E. If A is extreme in B and B is extreme in A, then A = B.

Русский

Пусть A и B — подмножества пространства E. Если A является крайним относительно B, а B — относительно A, то A = B.

LaTeX

$$$\forall A,B \subseteq E,\ IsExtreme 𝕜 A B \land IsExtreme 𝕜 B A \Rightarrow A = B$$$

Lean4

protected theorem antisymm : AntiSymmetric (IsExtreme 𝕜 : Set E → Set E → Prop) := fun _ _ hAB hBA ↦
  Subset.antisymm hBA.1 hAB.1

Похожие утверждения