mem_image_val_of_mem — Mathlib

English

If a ∈ β and ⟨a, ha⟩ ∈ γ, then a lies in the projection of γ onto α, i.e. a ∈ image Subtype.val γ.

Русский

Если a ∈ β и ⟨a, ha⟩ ∈ γ, то a принадлежит проекции γ на α, то есть a ∈ image Subtype.val γ.

LaTeX

$$$\Bigl( a \in \beta \Bigr) \land \bigl( \langle a, ha \rangle \in \gamma \bigr) \Rightarrow a \in \operatorname{image}(\operatorname{Subtype.val}) \gamma.$$$

Lean4

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

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