instIsPartialOrderSetIsExtreme — Mathlib

English

The relation IsExtreme 𝕜 on subsets of E defines a partial order on the power set of E.

Русский

Отношение IsExtreme 𝕜 на подмножествaх E задаёт частичный порядок над множествами-образами E.

LaTeX

$$$\text{IsExtreme}_{𝕜}$ is a partial order on the power set of $E$, i.e. $\forall A,B,C \subseteq E$, A\le B \land B\le C \Rightarrow A\le C$, $A\le A$; and if A\le B and B\le A then A=B.$$$

Lean4

instance : IsPartialOrder (Set E) (IsExtreme 𝕜)
    where
  refl := IsExtreme.refl 𝕜
  trans _ _ _ := IsExtreme.trans
  antisymm := IsExtreme.antisymm

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