English
There is an induction principle for inf'_ over finite sets: if p is closed under inf of two α-values and holds for all f(b) with b ∈ s, then p holds for s.inf' H f.
Русский
Существует принцип индукции по инф'_: если p замкнуто относительно инфимума двух значений и выполняется для всех f(b) с b ∈ s, то p выполняется для inf'_ над s.
LaTeX
$$$\\text{inf'_induction}_{H,f}(p) : (\\forall a_1,a_2, p(a_1) \\land p(a_2) \\Rightarrow p(a_1 \\inf a_2)) \\Rightarrow (\\forall b \\in s, p(f(b))) \\Rightarrow p(s.inf' H f)$$$
Lean4
theorem comp_inf'_eq_inf'_comp [SemilatticeInf γ] {s : Finset β} (H : s.Nonempty) {f : β → α} (g : α → γ)
(g_inf : ∀ x y, g (x ⊓ y) = g x ⊓ g y) : g (s.inf' H f) = s.inf' H (g ∘ f) :=
comp_sup'_eq_sup'_comp (α := αᵒᵈ) (γ := γᵒᵈ) H g g_inf
