mem_coe_of_mem — Mathlib

English

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

Русский

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

LaTeX

$$$a \in \gamma \quad\text{whenever } a \in \beta \text{ and } \langle a, ha \rangle \in \gamma$$$

Lean4

theorem mem_coe_of_mem {a : α} (ha : a ∈ β) (ha' : ⟨a, ha⟩ ∈ γ) : a ∈ (γ : Set α) :=
  ⟨_, ⟨⟨_, rfl⟩, _, ⟨ha', rfl⟩, rfl⟩⟩

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