mem_sup — Mathlib

English

For any finite set s of α, and a family f : α → Multiset β with DecidableEq β, an element x belongs to the supremum s.sup f if and only if there exists v ∈ s with x ∈ f(v).

Русский

Пусть s — конечный набор индексов α, f : α → Multiset β и [DecidableEq β]. Тогда x ∈ s.sup f тогда и только тогда, когда существует v ∈ s такое, что x ∈ f(v).

LaTeX

$$$x \\in s.\\mathrm{sup}\\ f \\iff \\exists v \\in s,\\ x \\in f(v).$$$

Lean4

theorem mem_sup {α β} [DecidableEq β] {s : Finset α} {f : α → Multiset β} {x : β} : x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v := by
  induction s using Finset.cons_induction <;> simp [*]

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