biInf_mem — Mathlib

English

If a finite set t of indices and f(i) ∈ L for all i ∈ t, then the biInf over i ∈ t of f(i) belongs to L.

Русский

Пусть t конечно; если для всех i ∈ t выполняется f(i) ∈ L, то биInf над i ∈ t of f(i) ∈ L.

LaTeX

$$$\\text{biInf\_mem} [Finite ι] (ht : t.Finite) (hf : \\forall i \\in t, f(i) \\in L) : (\\bigwedge_{i \\in t} f(i)) \\in L$$$

Lean4

theorem biInf_mem {ι : Type*} {t : Set ι} {f : ι → α} (ht : t.Finite) (hf : ∀ i ∈ t, f i ∈ L) : ⨅ i ∈ t, f i ∈ L :=
  L.infClosed.biInf_mem ht top_mem hf

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