mem_of_mem_coe

Mathlib.Data.Set.Functor

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

English

If a ∈ β and ⟨a, ha⟩ ∈ γ, then a ∈ γ as a subset of α.

Русский

Если a ∈ β и ⟨a, ha⟩ ∈ γ, то a ∈ γ как подмножество α.

LaTeX

$$$a \in \gamma \text{ if } a \in \beta \text{ and } ⟨a, ha⟩ \in γ$$$

Lean4

theorem mem_of_mem_coe {a : α} (ha : a ∈ (γ : Set α)) : ⟨a, coe_subset ha⟩ ∈ γ := by
  rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩; convert ha

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

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

Разделы

Аффилиация

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