`Finset.measurable_inf'`🔗

Theorem

Dual version of Finset.measurable_sup'.

Types

α : Type u_1SemilatticeInf αA SemilatticeInf is a meet-semilattice, that is, a partial order with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation ⊓ which is the greatest element smaller than both factors.m : MeasurableSpace αA measurable space is a space equipped with a σ-algebra.MeasurableInf₂ αWe say that a type has MeasurableInf₂ if uncurry (· ⊓ ·) is a measurable functions.
δ : Type u_2MeasurableSpace δ
ι : Type u_3

Given

s : Finset ιFinset α is the type of finite sets of elements of α.
f : ι → δ → α

Assuming

hs : s.NonemptyThe property s.Nonempty expresses the fact that the finset s is not empty.
hf : ∀ n ∈ s, Measurable (f n)A function f between measurable spaces is measurable if the preimage of every measurable set is measurable.

Then

Measurable (s.inf' hs f)

SemilatticeInf : Type u → Type u

A `SemilatticeInf` is a meet-semilattice, that is, a partial order
with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation
`⊓` which is the greatest element smaller than both factors.

MeasurableSpace : Type u_6 → Type u_6

A measurable space is a space equipped with a σ-algebra.

MeasurableInf₂ : (M : Type u_1) → [MeasurableSpace M] → [Min M] → Prop

We say that a type has `MeasurableInf₂` if `uncurry (· ⊓ ·)` is a measurable functions.
For a typeclass assuming measurability of `(c ⊓ ·)` and `(· ⊓ c)` see `MeasurableInf`.

Finset : Type u_3 → Type u_3

`Finset α` is the type of finite sets of elements of `α`. It is implemented
as a multiset (a list up to permutation) which has no duplicate elements.

Finset.Nonempty : {α : Type u_1} → Finset α → Prop

The property `s.Nonempty` expresses the fact that the finset `s` is not empty. It should be used
in theorem assumptions instead of `∃ x, x ∈ s` or `s ≠ ∅` as it gives access to a nice API thanks
to the dot notation.

Measurable : {α : Type u_1} → {β : Type u_2} → [MeasurableSpace α] → [MeasurableSpace β] → (α → β) → Prop

A function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.

Finset.inf' : {α : Type u_2} → {β : Type u_3} → [SemilatticeInf α] → (s : Finset β) → s.Nonempty → (β → α) → α

Given nonempty finset `s` then `s.inf' H f` is the infimum of its image under `f` in (possibly
unbounded) meet-semilattice `α`, where `H` is a proof of nonemptiness. If `α` has a top element you
may instead use `Finset.inf` which does not require `s` nonempty.

Code

theorem Finset.measurable_inf' {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {f : ι → δ → α}
    (hf : ∀ n ∈ s, Measurable (f n)) : Measurable (s.inf' hs f)

Proof

Finset.inf'_induction hs _ (fun _f hf _g hg => hf.inf hg) fun n hn => hf n hn

Actions: Source · Open Issue

Meaning unchanged since v4.33.0-rc1-29-gce231eb, the oldest revision on record (2026-07-30).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Nothing to draw. Its statement rests on no other declaration in this project, and names nothing from a package left unaudited — so the graph is this declaration alone. That is the answer, not a missing picture.

Audit surface: 0 project declarations, 12 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

Finset.measurable_inf'🔗

`Finset.measurable_inf'`🔗