top_mul_of_one_le — Mathlib

English

If 1 ≤ f, then ⊤ * f = ⊤; multiplication by a nontrivial filter preserves top.

Русский

Если 1 ≤ f, то ⊤ * f = ⊤; умножение верхнего фильтра на непустый фильтр сохраняет верхний.

LaTeX

$$$\forall f \in \mathrm{Filter}(\alpha),\ 1 \le f \Rightarrow (\top * f) = \top.$$$

Lean4

@[to_additive]
theorem top_mul_of_one_le (hf : 1 ≤ f) : ⊤ * f = ⊤ :=
  by
  refine top_le_iff.1 fun s => ?_
  simp only [mem_mul, mem_top, exists_eq_left]
  rintro ⟨t, ht, hs⟩
  rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

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