instIsIrreflSSubset — Mathlib

English

Strict subset is irreflexive: no Finset is strictly contained in itself.

Русский

Строгое подmножество иррефлексивно: ни одно Finset не является строго подмножество самого себя.

LaTeX

$$instance : IsIrrefl (Finset α) (· ⊂ ·) := show IsIrrefl (Finset α) (· < ·) by infer_instance$$

Lean4

instance : IsIrrefl (Finset α) (· ⊂ ·) :=
  show IsIrrefl (Finset α) (· < ·) by infer_instance

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