lift'_inf_principal_eq — Mathlib

English

For any h: Set α → Set β and any s ⊆ β, we have (f.lift' h) ∧ 𝓟 s = f.lift' (t ↦ h t ∩ s).

Русский

Для любой h: Set α → Set β и любого s ⊆ β выполняется (f.lift' h) ∧ 𝓟 s = f.lift' (t ↦ h t ∩ s).

LaTeX

$$$(f.lift' h) \\wedge 𝓟 s = f.lift'(\\lambda t. h t \\cap s)$$$

Lean4

theorem lift'_inf_principal_eq {h : Set α → Set β} {s : Set β} : f.lift' h ⊓ 𝓟 s = f.lift' fun t => h t ∩ s := by
  simp only [Filter.lift', Filter.lift, (· ∘ ·), ← inf_principal, iInf_subtype', ← iInf_inf]

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