inf_induction — Mathlib

English

If a property p holds at top and is closed under inf, and holds for all f b for b ∈ s, then p(s.inf f).

Русский

Если свойство p верно для верхней границы и сохраняется под инф, и если выполняется p(f(b)) для каждого b в s, то p(inf_{b∈s} f(b)).

LaTeX

$$$ p(\\top) \\to (\\forall a_1 a_2, p(a_1) \\to p(a_2) \\to p(a_1 \\inf a_2)) \\to (\\forall b \\in s, p(f(b))) \\to p(s.\\inf f)$$$

Lean4

theorem inf_induction {p : α → Prop} (ht : p ⊤) (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊓ a₂)) (hs : ∀ b ∈ s, p (f b)) :
    p (s.inf f) :=
  @sup_induction αᵒᵈ _ _ _ _ _ _ ht hp hs

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