inf'_induction — Mathlib

English

If s is a set closed under binary infimum, and t is a nonempty finite index set with p(i) ∈ s for all i ∈ t, then the infimum t.inf' H p belongs to s.

Русский

Если s замкнуто относительно бинарного инфимума, и t — непустое конечное множество индексов с p(i) ∈ s для всех i ∈ t, то t.inf' H p ∈ s.

LaTeX

$$$t.inf' H p \\in s \\quad\\text{whenever } (\\forall i \\in t, p(i) \\in s) \\text{ and } w: (x,y) \\mapsto x \\inf y \\in s$$$

Lean4

theorem inf'_induction {p : α → Prop} (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊓ a₂)) (hs : ∀ b ∈ s, p (f b)) :
    p (s.inf' H f) :=
  sup'_induction (α := αᵒᵈ) H f hp hs

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