mem_sup' — Mathlib

English

For a nonempty Finset s and a family f : ι → Finset α, an element a belongs to s.sup' hs f if and only if there exists i ∈ s with a ∈ f(i).

Русский

Пусть s — ненулевой Finset, f : ι → Finset α. Тогда a ∈ s.sup' hs f эквивалентно существованию i ∈ s такое, что a ∈ f(i).

LaTeX

$$$a \\in s.sup'\\, hs\\, f \\iff \\exists i \\in s,\\ a \\in f(i).$$$

Lean4

@[simp]
theorem mem_sup' (hs) : a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i := by induction hs using Nonempty.cons_induction <;> simp [*]

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