mem_inf' — Mathlib

English

For a nonempty Finset s and a family f : ι → Finset α, an element a belongs to s.inf' hs f if and only if a ∈ f(i) for all i ∈ s.

Русский

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

LaTeX

$$$a \\in s.inf'\\, hs\\, f \\iff ∀ i \\in s,\\ a ∈ f(i).$$$

Lean4

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

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