le_filter — Mathlib

English

Characterization of submultisets under filtering: s ≤ filter p t iff s ≤ t and ∀ a ∈ s, p a.

Русский

Характеризация подмультимножества под фильтрацией: s ≤ filter p t эквивалентно s ≤ t и ∀ a ∈ s, p a.

LaTeX

$$$\\left( s \\le \\mathrm{filter}_p(t) \\right) \\iff \\left( s \\le t \\land \\forall a \\in s, p(a) \\right)$$$

Lean4

theorem le_filter {s t} : s ≤ filter p t ↔ s ≤ t ∧ ∀ a ∈ s, p a :=
  ⟨fun h => ⟨le_trans h (filter_le _ _), fun _a m => of_mem_filter (mem_of_le h m)⟩, fun ⟨h, al⟩ =>
    filter_eq_self.2 al ▸ filter_le_filter p h⟩

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