mul_top_of_one_le — Mathlib

English

(⊤ : Filter α)^n = ⊤ for all n ≠ 0.

Русский

(⊤ : Filter α)^n = ⊤ для любого n ≠ 0.

LaTeX

$$$\forall n \in \mathbb{N},\ n \neq 0 \Rightarrow (\top : \mathrm{Filter}(\alpha))^n = \top.$$$

Lean4

@[to_additive]
theorem mul_top_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 [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

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