coe_subset_coe — Mathlib

English

The subset relation on interval endpoints corresponds to the order on intervals: (s:Set α) ⊆ t iff s ≤ t.

Русский

Отношение подмножества на множествах интервалов соответствует порядку между интервалами: (s:Set α) ⊆ t iff s ≤ t.

LaTeX

$$$ (s : \mathrm{Set}(\alpha)) \subseteq t \iff s \le t $$$

Lean4

@[norm_cast]
theorem coe_subset_coe : (s : Set α) ⊆ t ↔ s ≤ t :=
  (@coeHom α _).le_iff_le

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