coe_subset_coe

Mathlib.Data.SetLike.Basic

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

English

For S,T ∈ A, the coerced subset (S : Set B) is contained in T if and only if S ≤ T in the SetLike order.

Русский

Для S,T ∈ A подмножество, полученное через приведение к Set B, содержится в T тогда, когда S ≤ T в порядке SetLike.

LaTeX

$$$ (S : Set B) \\subseteq T \\iff S \\le T $$$

Lean4

@[simp, norm_cast]
theorem coe_subset_coe {S T : A} : (S : Set B) ⊆ T ↔ S ≤ T :=
  .rfl

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

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

Разделы

Аффилиация

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