mem_restrict — Mathlib

English

Membership in a restricted part equals conjunction of the condition and membership in the ambient part.

Русский

Членство в ограниченной части равно конъюнкции условия и членство в внешнем множестве.

LaTeX

$$$a \\in \\restrict p\\ o\\ h \\leftrightarrow p \\land a \\in o$.$$

Lean4

@[simp]
theorem mem_restrict (p : Prop) (o : Part α) (h : p → o.Dom) (a : α) : a ∈ restrict p o h ↔ p ∧ a ∈ o :=
  by
  dsimp [restrict, mem_eq]; constructor
  · rintro ⟨h₀, h₁⟩
    exact ⟨h₀, ⟨_, h₁⟩⟩
  rintro ⟨h₀, _, h₂⟩; exact ⟨h₀, h₂⟩

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