coe_subset

Mathlib.Data.Set.Functor

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

English

The coercion of γ (a subset of β) to Set α is contained in β: (γ : Set α) ⊆ β.

Русский

Переобразование γ (множество из β) в Set α содержится в β: (γ : Set α) ⊆ β.

LaTeX

$$$(\gamma : Set \alpha) \subseteq \beta$$$

Lean4

theorem coe_subset : (γ : Set α) ⊆ β := by intro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩; convert ha

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

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

Разделы

Аффилиация

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