proposition: Lemma preserves_in `{FullFSet A} `{FullFSet B} (f : A → B) `{!Inverse f} `{!Bijective f} x X : f x ∈ fset_map f X ↔ x ∈ X.
proof: Proof. pose proof (injective_mor f). pose proof (join_sl_mor_preserving (fset_map f)). pose proof (join_sl_mor_reflecting (fset_map f)). rewrite !fset_in_singleton_le. split; intros E. apply (order_reflecting (fset_map f)). now rewrite <-(fset_map_correct_applied f). rewrite (fset_map_correct_applied f). now apply (order_preserving _). Qed.
imports: MathClasses.theory.lattices MathClasses.varieties.monoids MathClasses.implementations.bool MathClasses.implementations.list_finite_set MathClasses.orders.lattices MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders