ssubset_iff_of_subset — Mathlib

English

Let S and T be subsets with S ⊆ T. Then S ⊊ T if and only if there exists x ∈ T such that x ∉ S.

Русский

Пусть S, T — подмножества множества α. Пусть S ⊆ T. Тогда S ⊊ T тогда и только тогда существует x ∈ T, такой что x ∉ S.

LaTeX

$$$ (s \subseteq t) \Rightarrow (s \subsetneq t \iff \exists x \in t, x \notin s)$$$

Lean4

theorem ssubset_iff_of_subset {s t : Set α} (h : s ⊆ t) : s ⊂ t ↔ ∃ x ∈ t, x ∉ s :=
  ⟨exists_of_ssubset, fun ⟨_, hxt, hxs⟩ => ⟨h, fun h => hxs <| h hxt⟩⟩

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