Theorems · Theorem

Function.HasFiniteSupport.iInf

∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : ConditionallyCompleteLattice M] {ι : Sort u_3} [Nonempty ι]
  [Finite ι] {f : ι → α → M},
  (∀ (i : ι), Function.HasFiniteSupport (f i)) → Function.HasFiniteSupport fun a => ⨅ i, f i a

Defined in: Mathlib.Algebra.FiniteSupport.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Zero ConditionallyCompleteLattice Nonempty Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finitestatement and proof · cited by 3,029
iInfstatement · cited by 1,690
ConditionallyCompleteLatticestatement and proof · cited by 364
Set.Finite.subsetproof · cited by 285
Function.HasFiniteSupportstatement and proof · cited by 113
Set.finite_iUnionproof · cited by 14
Function.support_iInfproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.