instTransSSubset — Mathlib

English

The strict subset relation is transitive when composed with itself: if S ⊊ T and T ⊊ U, then S ⊊ U.

Русский

Строгое подмножество сохраняет транзитивность при повторной композиции: если S ⊊ T и T ⊊ U, то S ⊊ U.

LaTeX

$$$\\forall S,T,U\\subseteq\\alpha, (S\\subset T) \\land (T\\subset U) \\Rightarrow (S\\subset U)$$$

Lean4

instance : Trans ((· ⊂ ·) : Set α → Set α → Prop) (· ⊂ ·) (· ⊂ ·) :=
  show Trans (· < ·) (· < ·) (· < ·) by infer_instance

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