coe_sSubset_coe — Mathlib

English

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

Русский

Строгое подмножество для множеств интервалов соответствует строгому порядку между интервалами: (s:Set α) ⊂ t iff s < t.

LaTeX

$$$ (s : \mathrm{Set}(\alpha)) \subset t \iff s < t $$$

Lean4

@[norm_cast]
theorem coe_sSubset_coe : (s : Set α) ⊂ t ↔ s < t :=
  (@coeHom α _).lt_iff_lt

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