coe_ssubset_coe — Mathlib

English

Strict order on intervals corresponds to strict subset of the underlying sets: s < t iff (s as Set) ⊂ (t as Set).

Русский

Строгий порядок на интервалах соответствует строгому включению подмножеств: s < t тогда и только если (s как множество) ⊂ (t как множество).

LaTeX

$$$ (s : Set\,α) \subset (t : Set\,α) \iff s < t $$$

Lean4

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

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