choice_isFunc — Mathlib

English

If ∅ ∉ x, then there exists a function from ⋃ x to x.choice selecting a member for each element: IsFunc x (⋃₀ x) (choice x).

Русский

Если ∅ не принадлежит x, существует функция от ⋃ x к x.choice, выбирающая элемент из каждого множества: IsFunc x (⋃ x) (choice x).

LaTeX

$$$ \\text{choice\_isFunc} (h) : \\; \\text{IsFunc } x \\ (\\bigcup x) \\ (\\mathrm{choice} x). $$$

Lean4

theorem choice_isFunc (h : ∅ ∉ x) : IsFunc x (⋃₀ x) (choice x) :=
  (@map_isFunc _ (Classical.allZFSetDefinable _) _ _).2 fun y yx => mem_sUnion.2 ⟨y, yx, choice_mem_aux x h y yx⟩

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