ker_iSup — Mathlib

English

The kernel distributes over arbitrary suprema: ker (⨆ i, f i) = ⋃ i, ker (f i).

Русский

Ядро распределяется по произвольной верхней границе: ker(⨆ i, f i) = ⋃ i, ker(f i).

LaTeX

$$$\\ker\\big(\\bigsqcup_i f_i\\big) = \\bigcup_i \\ker(f_i)$$$

Lean4

@[simp]
theorem ker_iSup (f : ι → Filter α) : ker (⨆ i, f i) = ⋃ i, ker (f i) :=
  by
  refine subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup
  simp only [mem_iUnion, mem_ker] at hx ⊢
  contrapose! hx
  choose s hsf hxs using hx
  refine ⟨⋃ i, s i, ?_, by simpa⟩
  exact mem_iSup.2 fun i ↦ mem_of_superset (hsf i) (subset_iUnion s i)

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