coe_image_of_subset — Mathlib

English

If t ⊆ s, then the inclusion image of {x ∈ s | x ∈ t} equals t.

Русский

Если t ⊆ s, то образ включения множества {x ∈ s | x ∈ t} равен t.

LaTeX

$$$ (\uparrow) '' \{ x \in s \mid x \in t \} = t $$$

Lean4

@[simp]
theorem coe_image_of_subset {s t : Set α} (h : t ⊆ s) : (↑) '' {x : ↥s | ↑x ∈ t} = t :=
  by
  ext x
  rw [mem_image]
  exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩

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