instTransSubset — Mathlib

English

The subset relation on sets is transitive as an instance; i.e., if S ⊆ T and T ⊆ U, then S ⊆ U.

Русский

Подмножество на множествах образует транзитивность как инстанс: если S ⊆ T и T ⊆ U, то S ⊆ U.

LaTeX

$$$(S \subseteq T) \land (T \subseteq U) \Rightarrow S \subseteq U$$$

Lean4

instance : Trans ((· ⊆ ·) : Set α → Set α → Prop) (· ⊆ ·) (· ⊆ ·) :=
  show Trans (· ≤ ·) (· ≤ ·) (· ≤ ·) by infer_instance

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