mem_sup — Mathlib

English

Let s be a finite set of indices and f : ι → Finite sets α. Then a ∈ s.sup f iff ∃ i ∈ s, a ∈ f(i).

Русский

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

LaTeX

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

Lean4

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

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