coe_inclusion

Mathlib.Data.Set.Inclusion

URI: https://scilib.ai/kg/mathlib#Set.coe_inclusion

English

For h: s ⊆ t, and x ∈ s, the underlying α-value of inclusion(h)(x) equals the α-value of x.

Русский

Для h: s ⊆ t и x ∈ s, подлежащие значения α удовлетворяют (inclusion(h)(x))_α = x_α.

LaTeX

$$$(\mathrm{inclusion}(h)\,x : \alpha) = (x : \alpha).$$$

Lean4

@[simp]
theorem coe_inclusion (h : s ⊆ t) (x : s) : (inclusion h x : α) = (x : α) :=
  rfl

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

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

Разделы

Аффилиация

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