eq_of_inclusion_surjective — Mathlib

English

Let s,t be subsets of α with h: s ⊆ t. If the inclusion map is surjective, then s = t.

Русский

Пусть s,t — подмножества α и h: s ⊆ t. Если отображение включения сюръективно, то s = t.

LaTeX

$$$\text{Surjective}(\mathrm{inclusion}(h)) \Rightarrow s = t.$$$

Lean4

theorem eq_of_inclusion_surjective {s t : Set α} {h : s ⊆ t} (h_surj : Function.Surjective (inclusion h)) : s = t :=
  by
  refine Set.Subset.antisymm h (fun x hx => ?_)
  obtain ⟨y, hy⟩ := h_surj ⟨x, hx⟩
  grind

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