partialOrder — Mathlib

English

Finite sets are ordered by inclusion: s ≤ t iff s ⊆ t; lt corresponds to strict inclusion; hence (≤) is reflexive and transitive, and antisymmetric holds.

Русский

Конечные множества упорядочены включением: s ≤ t тогда и только тогда s ⊆ t; отношение «меньше» — строгое включение; выполняются рефлексивность, транзитивность и антисимметрия.

LaTeX

$$PartialOrder (Finset α)$$

Lean4

instance partialOrder : PartialOrder (Finset α) where
  le := (· ⊆ ·)
  lt := (· ⊂ ·)
  le_refl _ _ := id
  le_trans _ _ _ hst htu _ ha := htu <| hst ha
  le_antisymm _ _ hst hts := ext fun _ => ⟨@hst _, @hts _⟩

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