eq_univ_of_coe_eq

Mathlib.Data.Set.Functor

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

English

If (γ : Set α) equals β, then γ equals univ in Set β (i.e., γ is all of β).

Русский

Если (γ : Set α) равно β, то γ = univ в Set β (то есть γ — вся β).

LaTeX

$$$(\gamma : Set \alpha) = \beta \Rightarrow \gamma = \mathrm{univ}$$$

Lean4

theorem eq_univ_of_coe_eq (hγ : (γ : Set α) = β) : γ = univ :=
  eq_univ_of_forall fun ⟨_, ha⟩ => mem_of_mem_coe <| hγ.symm ▸ ha

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

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

Разделы

Аффилиация

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