instIsIrreflSSubset — Mathlib

English

The strict subset relation is irreflexive: no set is a strict subset of itself.

Русский

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

LaTeX

$$$\\forall S \\subseteq\\alpha,\\\\\\\ \\neg (S\\subsetneq S)$$$

Lean4

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

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