instIsNonstrictStrictOrderSubsetSSubset

English

The collection of subsets of α carries a nonstrict-strict order given by ⊆ and ⊂, i.e., inclusion and strict inclusion are paired as a consistent order.

Русский

Множество подмножеств α образует пару отношений с неплотной/строгой частью порядка: ⊆ и ⊂ образуют корректный порядок.

LaTeX

$$$\\operatorname{IsNonstrictStrictOrder}(\\mathcal{P}(\\alpha), \\subseteq, \\subsetneq)$$$

Lean4

instance : IsNonstrictStrictOrder (Set α) (· ⊆ ·) (· ⊂ ·) :=
  ⟨fun _ _ => Iff.rfl⟩
    -- TODO(Jeremy): write a tactic to unfold specific instances of generic notation?

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