Ordered topological groups

Behavior of one-sided neighborhood filters under multiplication, inversion, and division in ordered topological groups.

@[simp]

theorem Filter.map_mul_left_nhdsGT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousMul H] {c a : H} : map (fun (x : H) => c * x) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (c * a) (Set.Ioi (c * a))

@[simp]

theorem Filter.map_add_left_nhdsGT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousAdd H] {c a : H} : map (fun (x : H) => c + x) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (c + a) (Set.Ioi (c + a))

@[simp]

theorem Filter.map_mul_left_nhdsLT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousMul H] {c a : H} : map (fun (x : H) => c * x) (nhdsWithin a (Set.Iio a)) = nhdsWithin (c * a) (Set.Iio (c * a))

@[simp]

theorem Filter.map_add_left_nhdsLT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousAdd H] {c a : H} : map (fun (x : H) => c + x) (nhdsWithin a (Set.Iio a)) = nhdsWithin (c + a) (Set.Iio (c + a))

@[simp]

theorem Filter.map_mul_right_nhdsGT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousMul H] {c a : H} : map (fun (x : H) => x * c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a * c) (Set.Ioi (a * c))

@[simp]

theorem Filter.map_add_right_nhdsGT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousAdd H] {c a : H} : map (fun (x : H) => x + c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a + c) (Set.Ioi (a + c))

@[simp]

theorem Filter.map_mul_right_nhdsLT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousMul H] {c a : H} : map (fun (x : H) => x * c) (nhdsWithin a (Set.Iio a)) = nhdsWithin (a * c) (Set.Iio (a * c))

@[simp]

theorem Filter.map_add_right_nhdsLT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousAdd H] {c a : H} : map (fun (x : H) => x + c) (nhdsWithin a (Set.Iio a)) = nhdsWithin (a + c) (Set.Iio (a + c))

@[simp]

theorem Filter.inv_nhdsGT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : (nhdsWithin a (Set.Ioi a))⁻¹ = nhdsWithin a⁻¹ (Set.Iio a⁻¹)

@[simp]

theorem Filter.neg_nhdsGT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : -nhdsWithin a (Set.Ioi a) = nhdsWithin (-a) (Set.Iio (-a))

@[simp]

theorem Filter.inv_nhdsLT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : (nhdsWithin a (Set.Iio a))⁻¹ = nhdsWithin a⁻¹ (Set.Ioi a⁻¹)

@[simp]

theorem Filter.neg_nhdsLT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : -nhdsWithin a (Set.Iio a) = nhdsWithin (-a) (Set.Ioi (-a))

theorem tendsto_inv_nhdsGT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Ioi a)) (nhdsWithin a⁻¹ (Set.Iio a⁻¹))

theorem tendsto_neg_nhdsGT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Ioi a)) (nhdsWithin (-a) (Set.Iio (-a)))

theorem tendsto_inv_nhdsLT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Iio a)) (nhdsWithin a⁻¹ (Set.Ioi a⁻¹))

theorem tendsto_neg_nhdsLT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Iio a)) (nhdsWithin (-a) (Set.Ioi (-a)))

theorem tendsto_inv_nhdsGT_inv {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Ioi a⁻¹)) (nhdsWithin a (Set.Iio a))

theorem tendsto_neg_nhdsGT_neg {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ioi (-a))) (nhdsWithin a (Set.Iio a))

theorem tendsto_inv_nhdsLT_inv {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iio a⁻¹)) (nhdsWithin a (Set.Ioi a))

theorem tendsto_neg_nhdsLT_neg {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iio (-a))) (nhdsWithin a (Set.Ioi a))

theorem tendsto_inv_nhdsGE {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Ici a)) (nhdsWithin a⁻¹ (Set.Iic a⁻¹))

theorem tendsto_neg_nhdsGE {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Ici a)) (nhdsWithin (-a) (Set.Iic (-a)))

theorem tendsto_inv_nhdsLE {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a (Set.Iic a)) (nhdsWithin a⁻¹ (Set.Ici a⁻¹))

theorem tendsto_neg_nhdsLE {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin a (Set.Iic a)) (nhdsWithin (-a) (Set.Ici (-a)))

theorem tendsto_inv_nhdsGE_inv {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Ici a⁻¹)) (nhdsWithin a (Set.Iic a))

theorem tendsto_neg_nhdsGE_neg {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ici (-a))) (nhdsWithin a (Set.Iic a))

theorem tendsto_inv_nhdsLE_inv {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iic a⁻¹)) (nhdsWithin a (Set.Ici a))

theorem tendsto_neg_nhdsLE_neg {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] [ContinuousNeg H] {a : H} : Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iic (-a))) (nhdsWithin a (Set.Ici a))

theorem tendsto_inv_nhdsWithin_Iic_inv {H : Type u_1} [TopologicalSpace H] [CommGroup H] [PartialOrder H] [IsOrderedMonoid H] [ContinuousInv H] {a : H} : Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iic a⁻¹)) (nhdsWithin a (Set.Ici a))

Alias of tendsto_inv_nhdsLE_inv.

@[simp]

theorem Filter.map_divRight_nhdsGT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [IsTopologicalGroup H] [PartialOrder H] [IsOrderedMonoid H] {c a : H} : map (fun (x : H) => x / c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a / c) (Set.Ioi (a / c))

@[simp]

theorem Filter.map_subRight_nhdsGT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [IsTopologicalAddGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {c a : H} : map (fun (x : H) => x - c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a - c) (Set.Ioi (a - c))

@[simp]

theorem Filter.map_divRight_nhdsLT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [IsTopologicalGroup H] [PartialOrder H] [IsOrderedMonoid H] {c a : H} : map (fun (x : H) => x / c) (nhdsWithin a (Set.Iio a)) = nhdsWithin (a / c) (Set.Iio (a / c))

@[simp]

theorem Filter.map_subRight_nhdsLT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [IsTopologicalAddGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {c a : H} : map (fun (x : H) => x - c) (nhdsWithin a (Set.Iio a)) = nhdsWithin (a - c) (Set.Iio (a - c))

@[simp]

theorem Filter.map_divLeft_nhdsGT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [IsTopologicalGroup H] [PartialOrder H] [IsOrderedMonoid H] {c a : H} : map (fun (x : H) => c / x) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (c / a) (Set.Iio (c / a))

@[simp]

theorem Filter.map_subLeft_nhdsGT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [IsTopologicalAddGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {c a : H} : map (fun (x : H) => c - x) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (c - a) (Set.Iio (c - a))

@[simp]

theorem Filter.map_divLeft_nhdsLT {H : Type u_1} [TopologicalSpace H] [CommGroup H] [IsTopologicalGroup H] [PartialOrder H] [IsOrderedMonoid H] {c a : H} : map (fun (x : H) => c / x) (nhdsWithin a (Set.Iio a)) = nhdsWithin (c / a) (Set.Ioi (c / a))

@[simp]

theorem Filter.map_subLeft_nhdsLT {H : Type u_1} [TopologicalSpace H] [AddCommGroup H] [IsTopologicalAddGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {c a : H} : map (fun (x : H) => c - x) (nhdsWithin a (Set.Iio a)) = nhdsWithin (c - a) (Set.Ioi (c - a))