choice_mem — Mathlib

English

For h : ∅ ∉ x, and y ∈ x, the chosen element for y belongs to y: (choice x′ y) ∈ y.

Русский

Пусть ∅ ∉ x и y ∈ x; выбранный элемент для y принадлежит y: (choice x′ y) ∈ y.

LaTeX

$$$ (\\mathrm{choice}\\ x'\\ y : \\mathrm{Class}) \\in (y : \\mathrm{Class}). $$$

Lean4

theorem choice_mem (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) : (choice x ′ y : Class.{u}) ∈ (y : Class.{u}) :=
  by
  delta choice
  rw [@map_fval _ (Classical.allZFSetDefinable _) x y yx, Class.coe_mem, Class.coe_apply]
  exact choice_mem_aux x h y yx

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