coe_ssubset_coe

Mathlib.Data.SetLike.Basic

URI: https://scilib.ai/kg/mathlib#SetLike.coe_ssubset_coe

English

For any S, T in the SetLike structure, the strict subset relation (S ⊂ T) corresponds to the strict order on the carriers: (S : Set B) ⊂ T ↔ S < T.

Русский

Для S, T в структуре SetLike равносильно строгому включению подмножества: (S : Set B) ⊂ T ↔ S < T.

LaTeX

$$$ (S : Set B) \subset T \iff S < T $$$

Lean4

@[simp, norm_cast]
theorem coe_ssubset_coe {S T : A} : (S : Set B) ⊂ T ↔ S < T :=
  .rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru