mem_piFinset — Mathlib

English

An element f belongs to piFinset t iff for every a, f(a) ∈ t(a).

Русский

Элемент f принадлежит piFinset t тогда, когда для каждого a выполняется f(a) ∈ t(a).

LaTeX

$$$f \\in \\mathrm{piFinset}(t) \\iff \\forall a, f(a) \\in t(a)$$$

Lean4

@[simp]
theorem mem_piFinset {t : ∀ a, Finset (δ a)} {f : ∀ a, δ a} : f ∈ piFinset t ↔ ∀ a, f a ∈ t a :=
  by
  constructor
  · simp only [piFinset, mem_map, and_imp, forall_prop_of_true, mem_univ, exists_imp, mem_pi]
    rintro g hg hgf a
    rw [← hgf]
    exact hg a
  · simp only [piFinset, mem_map, forall_prop_of_true, mem_univ, mem_pi]
    exact fun hf => ⟨fun a _ => f a, hf, rfl⟩

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