inf_ind — Mathlib

English

Let a and b be elements of a linear order α, and let p be a predicate on α. If p(a) holds and p(b) holds, then p(a ∧ b) holds.

Русский

Пусть a и b — элементы линейного порядка α, p — предикат на α. Если p(a) и p(b) выполняются, то p(a ∧ b) выполняется.

LaTeX

$$$ \forall a,b:\, α,\ p(a) \rightarrow p(b) \rightarrow p(a \sqcap b) $$$

Lean4

theorem inf_ind (a b : α) {p : α → Prop} : p a → p b → p (a ⊓ b) :=
  @sup_ind αᵒᵈ _ _ _ _

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