mem_mk — Mathlib

English

Membership of a subset in the constructed filter mk t h₁ h₂ h₃ is exactly membership in t.

Русский

Членство подмножества в сконструированном фильтре mk t h₁ h₂ h₃ точно равно членству в t.

LaTeX

$$$\forall {t:Set(Set\alpha)} {h_1,h_2,h_3},\ s\in mk\ t\ h_1\ h_2\ h_3 \iff s\in t$$$

Lean4

@[simp]
protected theorem mem_mk {t : Set (Set α)} {h₁ h₂ h₃} : s ∈ mk t h₁ h₂ h₃ ↔ s ∈ t :=
  Iff.rfl

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