forall_iff — Mathlib

English

If l has a basis p s and P is monotone with respect to subset, then (for all s ∈ l, P s) is equivalent to (for all i, p i → P(s i)).

Русский

Если l имеет базис p s и P монотонно по подмножествам, то (для всех s из l, P s) эквивалентно (для всех i, p i → P(s i)).

LaTeX

$$$(\forall s\in l, P s)\;\Leftrightarrow\; \forall i, p i \rightarrow P(s i)$$$

Lean4

theorem forall_iff (hl : l.HasBasis p s) {P : Set α → Prop} (mono : ∀ ⦃s t⦄, s ⊆ t → P s → P t) :
    (∀ s ∈ l, P s) ↔ ∀ i, p i → P (s i) :=
  ⟨fun H i hi => H (s i) <| hl.mem_of_mem hi, fun H _s hs =>
    let ⟨i, hi, his⟩ := hl.mem_iff.1 hs
    mono his (H i hi)⟩

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