congr_sets — Mathlib

English

If the set {x | x ∈ s ↔ x ∈ t} belongs to f, then s ∈ f ⇔ t ∈ f.

Русский

Если множество {x | x ∈ s ⇔ x ∈ t} принадлежит f, тогда s ∈ f ⇔ t ∈ f.

LaTeX

$$$\{x \mid x \in s \iff x \in t\} \in f \Rightarrow s \in f \iff t \in f$$$

Lean4

theorem congr_sets (h : {x | x ∈ s ↔ x ∈ t} ∈ f) : s ∈ f ↔ t ∈ f :=
  ⟨fun hs => mp_mem hs (mem_of_superset h fun _ => Iff.mp), fun hs => mp_mem hs (mem_of_superset h fun _ => Iff.mpr)⟩

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