instIsNonstrictStrictOrderSubsetSSubset

English

The pair of relations (≤, <) on Finset α forms a nonstrict-then-strict order: the order is compatible in the expected way.

Русский

Пара отношений (≤, <) на Finset α образует порядок, где нестрогий порядок совместим со строгим в ожидаемом смысле.

LaTeX

$$instance : IsNonstrictStrictOrder (Finset α) (· ⊆ ·) (· ⊂ ·) := ⟨fun _ _ => Iff.rfl⟩$$

Lean4

instance : IsNonstrictStrictOrder (Finset α) (· ⊆ ·) (· ⊂ ·) :=
  ⟨fun _ _ => Iff.rfl⟩

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