diff_mem_inf_principal_compl — Mathlib

English

If s ∈ f, then for every t, s \\ t ∈ f ⊓ 𝓟(t^c).

Русский

Если s принадлежит f, тогда для любого t множество s \\ t принадлежит f ⊓ 𝓟(t^c).

LaTeX

$$$s \\in f \\Rightarrow \\forall t, \\ (s \\setminus t) \\in f \\sqcap \\mathcal{P}(t^{c})$$$

Lean4

theorem diff_mem_inf_principal_compl {f : Filter α} {s : Set α} (hs : s ∈ f) (t : Set α) : s \ t ∈ f ⊓ 𝓟 tᶜ :=
  inter_mem_inf hs <| mem_principal_self tᶜ

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